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
Iris
Fairis
Commits
d40bbd57
Commit
d40bbd57
authored
Feb 17, 2016
by
Robbert Krebbers
Browse files
Document csimpl.
parent
0fd7e635
Changes
1
Show whitespace changes
Inline
Sidebyside
prelude/tactics.v
View file @
d40bbd57
...
...
@@ 117,7 +117,13 @@ does the converse. *)
Ltac
var_eq
x1
x2
:=
match
x1
with
x2
=>
idtac

_
=>
fail
1
end
.
Ltac
var_neq
x1
x2
:=
match
x1
with
x2
=>
fail
1

_
=>
idtac
end
.
(
**
Hacks
to
let
simpl
fold
type
class
projections
*
)
(
**
Operational
type
class
projections
in
recursive
calls
are
not
folded
back
appropriately
by
[
simpl
].
The
tactic
[
csimpl
]
uses
the
[
fold_classes
]
tactics
to
refold
recursive
calls
of
[
fmap
],
[
mbind
],
[
omap
]
and
[
alter
].
A
self

contained
example
explaining
the
problem
can
be
found
in
the
following
Coq

club
message
:
https:
//sympa.inria.fr/sympa/arc/coqclub/201210/msg00147.html *)
Ltac
fold_classes
:=
repeat
match
goal
with


appcontext
[
?
F
]
=>
...
...
@@ 160,7 +166,7 @@ Tactic Notation "csimpl" := try (progress simpl; fold_classes).
Tactic
Notation
"csimpl"
"in"
"*"
:=
repeat_on_hyps
(
fun
H
=>
csimpl
in
H
);
csimpl
.
(
*
The
tactic
[
simplify_eq
]
repeatedly
substitutes
,
discriminates
,
(
*
*
The
tactic
[
simplify_eq
]
repeatedly
substitutes
,
discriminates
,
and
injects
equalities
,
and
tries
to
contradict
impossible
inequalities
.
*
)
Tactic
Notation
"simplify_eq"
:=
repeat
match
goal
with
...
...
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