Skip to content
Snippets Groups Projects
Commit ff007045 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Improve a comment.

parent fe1efece
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
theories/proofmode/ltac_tactics.v
+ 2
− 2
View file @ ff007045
...@@ -127,8 +127,8 @@ pass arguments to Ssreflect's `rewrite` like `/= foo /bar` in Ltac, see: ...@@ -127,8 +127,8 @@ pass arguments to Ssreflect's `rewrite` like `/= foo /bar` in Ltac, see:
https://sympa.inria.fr/sympa/arc/coq-club/2018-01/msg00000.html 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 PMP told me (= Robbert) in person that this is not possible with the current
possible in Ltac2. *) Ltac, but it may be possible in Ltac2. *)
(** * Context manipulation *) (** * Context manipulation *)
Tactic Notation "iRename" constr(H1) "into" constr(H2) := Tactic Notation "iRename" constr(H1) "into" constr(H2) :=
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment