From ba8b9e94b65b6bc765af5d112ba63d81e2c5c6a0 Mon Sep 17 00:00:00 2001
From: Joseph Tassarotti <jtassaro@andrew.cmu.edu>
Date: Mon, 12 Mar 2018 07:43:03 -0400
Subject: [PATCH] iFresh: Force start proof when iFresh is called.

---
 theories/proofmode/coq_tactics.v |  4 ----
 theories/proofmode/tactics.v     | 23 ++++++++++++-----------
 2 files changed, 12 insertions(+), 15 deletions(-)

diff --git a/theories/proofmode/coq_tactics.v b/theories/proofmode/coq_tactics.v
index 561af06f7..953b7bd91 100644
--- a/theories/proofmode/coq_tactics.v
+++ b/theories/proofmode/coq_tactics.v
@@ -478,10 +478,6 @@ Global Instance envs_entails_flip_mono :
   Proper (envs_Forall2 (⊢) ==> flip (⊢) ==> flip impl) (@envs_entails PROP).
 Proof. rewrite envs_entails_eq=> Δ1 Δ2 ? P1 P2 <- <-. by f_equiv. Qed.
 
-Instance envs_incr_counter_proper :
-  Proper (envs_Forall2 (⊣⊢) ==> envs_Forall2 (⊣⊢)) (@envs_incr_counter PROP).
-Proof. intros ?? [? ?]; by constructor => //=. Qed.
-
 (** * Adequacy *)
 Lemma tac_adequate P : envs_entails (Envs Enil Enil 1) P → P.
 Proof.
diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index bbee041e1..113f48b31 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -40,17 +40,6 @@ Ltac iSolveTC :=
   solve [once (typeclasses eauto)].
 
 (** * Misc *)
-(* Tactic Notation tactics cannot return terms *)
-Ltac iFresh :=
-  lazymatch goal with
-  |- envs_entails ?Δ _ =>
-  let do_incr := (lazymatch goal with
-                    _ => eapply tac_fresh; first by (env_reflexivity)
-                  end) in
-    let n := eval env_cbv in (Pos.succ (env_counter Δ)) in
-    constr:(IAnon n)
-  | _ => constr:(IAnon 1)
-  end.
 
 Ltac iMissingHyps Hs :=
   let Δ :=
@@ -100,6 +89,18 @@ Tactic Notation "iStartProof" uconstr(PROP) :=
                |apply tac_adequate]
   end.
 
+(** * Generate a fresh identifier *)
+(* Tactic Notation tactics cannot return terms *)
+Ltac iFresh :=
+  let do_incr :=
+      lazymatch goal with
+      | _ => iStartProof; eapply tac_fresh; first by (env_reflexivity)
+      end in
+  lazymatch goal with
+  |- envs_entails ?Δ _ =>
+    let n := eval env_cbv in (env_counter Δ) in
+    constr:(IAnon n)
+  end.
 
 (** * Simplification *)
 Tactic Notation "iEval" tactic(t) :=
-- 
GitLab