diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index 113f48b31ff682e707ac4624776a6e52aedb8de8..ac5534879b1c299c8666f04b75a1f3c02eda3cc3 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)