From fa61a3c075c00bd56042d0f3f633f0b128cb22f7 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sun, 19 May 2019 17:19:23 +0200
Subject: [PATCH] Update documentation of [iFresh] and make sure it returns the
old counter.
---
theories/proofmode/ltac_tactics.v | 38 ++++++++++++++++++-------------
1 file changed, 22 insertions(+), 16 deletions(-)
diff --git a/theories/proofmode/ltac_tactics.v b/theories/proofmode/ltac_tactics.v
index 3018e07be..550db0c5e 100644
--- a/theories/proofmode/ltac_tactics.v
+++ b/theories/proofmode/ltac_tactics.v
@@ -91,25 +91,31 @@ Tactic Notation "iStartProof" uconstr(PROP) :=
end.
(** * Generate a fresh identifier *)
-(* Tactic Notation tactics cannot return terms *)
+(** The tactic [iFresh] bumps the fresh name counter in the proof mode
+environment and returns the old value.
+
+Note that we use [Ltac] instead of [Tactic Notation] since [Tactic Notation]
+tactics can only have side-effects, but cannot return terms. *)
Ltac iFresh :=
- (* We need to increment the environment counter using [tac_fresh].
- But because [iFresh] returns a value, we have to let bind
- [tac_fresh] wrapped under a match to force evaluation of this
- side-effect. See https://stackoverflow.com/a/46178884 *)
- let do_incr :=
+ (* We make use of an Ltac hack to allow the [iFresh] tactic to both have a
+ side-effect (i.e. to bump the counter) and to return a value (the fresh name).
+ We do this by wrapped the side-effect under a [match] in a let-binding. See
+ https://stackoverflow.com/a/46178884 *)
+ let _ :=
lazymatch goal with
- | _ =>
- iStartProof;
- lazymatch goal with
- | |- envs_entails (Envs ?Δp ?Δs ?c) ?Q =>
- let c' := eval vm_compute in (Pos.succ c) in
- convert_concl_no_check (envs_entails (Envs Δp Δs c') Q)
- end
+ | _ => iStartProof
end in
- lazymatch goal with
- |- envs_entails (Envs _ _ ?c) _ => constr:(IAnon c)
- end.
+ let c :=
+ lazymatch goal with
+ | |- envs_entails (Envs _ _ ?c) _ => c
+ end in
+ let _ :=
+ lazymatch goal with
+ | |- envs_entails (Envs ?Δp ?Δs _) ?Q =>
+ let c' := eval vm_compute in (Pos.succ c) in
+ convert_concl_no_check (envs_entails (Envs Δp Δs c') Q)
+ end in
+ constr:(IAnon c).
(** * Context manipulation *)
Tactic Notation "iRename" constr(H1) "into" constr(H2) :=
--
GitLab