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
Joshua Yanovski
iris-coq
Commits
04d70321
Commit
04d70321
authored
Feb 24, 2016
by
Ralf Jung
Browse files
make find_pat more robust: work with idtac
parent
73959011
Changes
1
Hide whitespace changes
Inline
Side-by-side
prelude/tactics.v
View file @
04d70321
...
...
@@ -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