Skip to content
GitLab
Projects
Groups
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
Simon Spies
Iris
Commits
4734d7bf
Commit
4734d7bf
authored
Feb 24, 2016
by
Robbert Krebbers
Browse files
Merge branch 'master' of gitlab.mpi-sws.org:FP/iris-coq
parents
4f1ed7c9
4dc4acae
Changes
1
Hide whitespace changes
Inline
Side-by-side
prelude/tactics.v
View file @
4734d7bf
...
...
@@ -303,7 +303,8 @@ Tactic Notation "feed" "destruct" constr(H) "as" simple_intropattern(IP) :=
It will search for the first subterm of the goal matching [pat], and then call [tac]
with that subterm. *)
Ltac
find_pat
pat
tac
:
=
match
goal
with
|-
context
[
?x
]
=>
unify
pat
x
;
tac
x
||
fail
2
match
goal
with
|-
context
[
?x
]
=>
unify
pat
x
;
tryif
tac
x
then
idtac
else
fail
2
end
.
(** Coq's [firstorder] tactic fails or loops on rather small goals already. In
...
...
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new 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