Skip to content
GitLab
Menu
Projects
Groups
Snippets
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
George Pirlea
Iris
Commits
1bc26dc9
Commit
1bc26dc9
authored
Nov 27, 2016
by
Robbert Krebbers
Browse files
Better error messages for iRevert.
This fixes issue #44.
parent
e4d5fc87
Changes
1
Hide whitespace changes
Inline
Sidebyside
proofmode/tactics.v
View file @
1bc26dc9
...
...
@@ 36,7 +36,7 @@ Tactic Notation "iTypeOf" constr(H) tactic(tac):=

Some
(
?p
,
?P
)
=>
tac
p
P
end
.
Ltac
iMatchGoal
tac
:
=
Tactic
Notation
"iMatchHyp"
tactic1
(
tac
)
:
=
match
goal
with


context
[
environments
.
Esnoc
_
?x
?P
]
=>
tac
x
P
end
.
...
...
@@ 431,11 +431,17 @@ Tactic Notation "iApply" open_constr(lem) :=
(** * Revert *)
Local
Tactic
Notation
"iForallRevert"
ident
(
x
)
:
=
let
err
x
:
=
intros
x
;
iMatchHyp
(
fun
H
P
=>
lazymatch
P
with

context
[
x
]
=>
fail
2
"iRevert:"
x
"is used in hypothesis"
H
end
)
in
let
A
:
=
type
of
x
in
lazymatch
type
of
A
with

Prop
=>
revert
x
;
apply
tac_pure_revert

_
=>
revert
x
;
apply
tac_forall_revert
end

fail
"iRevert: cannot revert"
x
.

Prop
=>
revert
x
;
first
[
apply
tac_pure_revert

err
x
]

_
=>
revert
x
;
first
[
apply
tac_forall_revert

err
x
]
end
.
Tactic
Notation
"iRevert"
constr
(
Hs
)
:
=
let
rec
go
Hs
:
=
...
...
@@ 1169,7 +1175,7 @@ Tactic Notation "iRewrite" "" open_constr(lem) "in" constr(H) :=
iRewriteCore
true
lem
in
H
.
Ltac
iSimplifyEq
:
=
repeat
(
iMatch
Goal
ltac
:
(
fun
H
P
=>
match
P
with
⌜
_
=
_
⌝
%
I
=>
iDestruct
H
as
%?
end
)
iMatch
Hyp
(
fun
H
P
=>
match
P
with
⌜
_
=
_
⌝
%
I
=>
iDestruct
H
as
%?
end
)

simplify_eq
/=).
(** * Update modality *)
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment