Commit d7f627fd authored by Joseph Tassarotti's avatar Joseph Tassarotti

iFresh: document the Ltac trick to force evaluation of the side-effect.

parent ba8b9e94
......@@ -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)
......
Markdown is supported
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