From d7f627fd6b155081290c08e783c291a763ee3124 Mon Sep 17 00:00:00 2001
From: Joseph Tassarotti <jtassaro@andrew.cmu.edu>
Date: Mon, 12 Mar 2018 21:25:02 -0400
Subject: [PATCH] iFresh: document the Ltac trick to force evaluation of the
side-effect.
---
theories/proofmode/tactics.v | 4 ++++
1 file changed, 4 insertions(+)
diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index 113f48b31..ac5534879 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -92,6 +92,10 @@ Tactic Notation "iStartProof" uconstr(PROP) :=
(** * Generate a fresh identifier *)
(* Tactic Notation tactics 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 :=
lazymatch goal with
| _ => iStartProof; eapply tac_fresh; first by (env_reflexivity)
--
GitLab