Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
What's new
7
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Open sidebar
Simon Spies
stdpp
Commits
35f7ca38
Commit
35f7ca38
authored
Feb 23, 2016
by
Ralf Jung
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
prove a tactic for canceling with pattern matching, and use it in a few (test-)places
parent
9df93b33
Changes
1
Hide whitespace changes
Inline
Side-by-side
Showing
1 changed file
with
8 additions
and
0 deletions
+8
-0
theories/tactics.v
theories/tactics.v
+8
-0
No files found.
theories/tactics.v
View file @
35f7ca38
...
...
@@ -298,6 +298,14 @@ Tactic Notation "feed" "destruct" constr(H) :=
Tactic
Notation
"feed"
"destruct"
constr
(
H
)
"as"
simple_intropattern
(
IP
)
:
=
feed
(
fun
p
=>
let
H'
:
=
fresh
in
pose
proof
p
as
H'
;
destruct
H'
as
IP
)
H
.
(** The following tactic can be used to add support for patterns to tactic notation:
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
end
.
(** Coq's [firstorder] tactic fails or loops on rather small goals already. In
particular, on those generated by the tactic [unfold_elem_ofs] which is used
to solve propositions on collections. The [naive_solver] tactic implements an
...
...
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