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
Iris
Iris
Commits
cd4706e8
Commit
cd4706e8
authored
Jan 16, 2018
by
Robbert Krebbers
Browse files
Add comment about `iSsrRewrite`.
parent
8b49eacf
Changes
1
Hide whitespace changes
Inline
Side-by-side
theories/proofmode/tactics.v
View file @
cd4706e8
...
...
@@ -96,6 +96,14 @@ Tactic Notation "iEval" tactic(t) "in" constr(H) :=
Tactic
Notation
"iSimpl"
:
=
iEval
simpl
.
Tactic
Notation
"iSimpl"
"in"
constr
(
H
)
:
=
iEval
simpl
in
H
.
(* It would be nice to also have an `iSsrRewrite`, however, for this we need to
pass arguments to Ssreflect's `rewrite` like `/= foo /bar` in Ltac, see:
https://sympa.inria.fr/sympa/arc/coq-club/2018-01/msg00000.html
PMP told me (= Robbert) in person that this is not possible today, but may be
possible in Ltac2. *)
(** * Context manipulation *)
Tactic
Notation
"iRename"
constr
(
H1
)
"into"
constr
(
H2
)
:
=
eapply
tac_rename
with
_
H1
H2
_
_;
(* (i:=H1) (j:=H2) *)
...
...
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