From e0492901ab388f6367f12528995111939fee99b6 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sun, 27 Jun 2021 20:16:44 +0200
Subject: [PATCH] add mk_evar tactic (to replace Coq's strange evar tactic) and
 use it

---
 theories/fin_maps.v  | 10 ++++------
 theories/gmultiset.v |  7 +++----
 theories/option.v    |  4 ++--
 theories/tactics.v   | 13 ++++++++++---
 4 files changed, 19 insertions(+), 15 deletions(-)

diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index 6295991c..1ed4cf3b 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -3198,10 +3198,9 @@ Tactic Notation "simpl_map" "by" tactic3(tac) := repeat
   | H : context[ (_ <$> _) !! _ ] |- _ => rewrite lookup_fmap in H
   | H : context[ (omap _ _) !! _ ] |- _ => rewrite lookup_omap in H
   | H : context[ lookup (A:=?A) ?i (?m1 ∪ ?m2) ] |- _ =>
-    let x := fresh in evar (x:A);
-    let x' := eval unfold x in x in clear x;
+    let x := mk_evar A in
     let E := fresh in
-    assert ((m1 ∪ m2) !! i = Some x') as E by (clear H; by tac);
+    assert ((m1 ∪ m2) !! i = Some x) as E by (clear H; by tac);
     rewrite E in H; clear E
   | |- context[ ∅ !! _ ] => rewrite lookup_empty
   | |- context[ (<[_:=_]>_) !! _ ] =>
@@ -3215,10 +3214,9 @@ Tactic Notation "simpl_map" "by" tactic3(tac) := repeat
   | |- context[ (_ <$> _) !! _ ] => rewrite lookup_fmap
   | |- context[ (omap _ _) !! _ ] => rewrite lookup_omap
   | |- context [ lookup (A:=?A) ?i ?m ] =>
-    let x := fresh in evar (x:A);
-    let x' := eval unfold x in x in clear x;
+    let x := mk_evar A in
     let E := fresh in
-    assert (m !! i = Some x') as E by tac;
+    assert (m !! i = Some x) as E by tac;
     rewrite E; clear E
   end.
 
diff --git a/theories/gmultiset.v b/theories/gmultiset.v
index eca07dc6..bb799aba 100644
--- a/theories/gmultiset.v
+++ b/theories/gmultiset.v
@@ -273,10 +273,9 @@ End multiset_unfold.
 Ltac multiset_instantiate :=
   repeat match goal with
   | H : (∀ x : ?A, @?P x) |- _ =>
-     let e := fresh in evar (e:A);
-     let e' := eval unfold e in e in clear e;
-     lazymatch constr:(P e') with
-     | context [ {[+ ?y +]} ] => unify y e'; learn_hyp (H y)
+     let e := mk_evar A in
+     lazymatch constr:(P e) with
+     | context [ {[+ ?y +]} ] => unify y e; learn_hyp (H y)
      end
   | H : (∀ x : ?A, _), _ : context [multiplicity ?y _] |- _ => learn_hyp (H y)
   | H : (∀ x : ?A, _) |- context [multiplicity ?y _] => learn_hyp (H y)
diff --git a/theories/option.v b/theories/option.v
index 0fd7dfaa..abdbf6f9 100644
--- a/theories/option.v
+++ b/theories/option.v
@@ -360,8 +360,8 @@ Proof. intros [??]. repeat case_option_guard; intuition. Qed.
 
 Tactic Notation "simpl_option" "by" tactic3(tac) :=
   let assert_Some_None A mx H := first
-    [ let x := fresh in evar (x:A); let x' := eval unfold x in x in clear x;
-      assert (mx = Some x') as H by tac
+    [ let x := mk_evar A in
+      assert (mx = Some x) as H by tac
     | assert (mx = None) as H by tac ]
   in repeat match goal with
   | H : context [@mret _ _ ?A] |- _ =>
diff --git a/theories/tactics.v b/theories/tactics.v
index 39543e5f..d3910a89 100644
--- a/theories/tactics.v
+++ b/theories/tactics.v
@@ -217,6 +217,14 @@ does the converse. *)
 Ltac var_eq x1 x2 := match x1 with x2 => idtac | _ => fail 1 end.
 Ltac var_neq x1 x2 := match x1 with x2 => fail 1 | _ => idtac end.
 
+(** The tactic [mk_evar T] returns a new evar of type [T], without affecting the
+current context.
+
+This is usually a more useful behavior than Coq's [evar], which is a
+side-effecting tactic (not returning anything) that introduces a local
+definition into the context that holds the evar. *)
+Ltac mk_evar T := open_constr:(_ : T).
+
 (** The tactic [eunify x y] succeeds if [x] and [y] can be unified, and fails
 otherwise. If it succeeds, it will instantiate necessary evars in [x] and [y].
 
@@ -483,9 +491,8 @@ Tactic Notation "efeed" constr(H) "using" tactic3(tac) "by" tactic3 (bytac) :=
     let HT1 := fresh "feed" in assert T1 as HT1;
       [bytac | go (H HT1); clear HT1 ]
   | ?T1 → _ =>
-    let e := fresh "feed" in evar (e:T1);
-    let e' := eval unfold e in e in
-    clear e; go (H e')
+    let e := mk_evar T1 in
+    go (H e)
   | ?T1 => tac H
   end in go H.
 Tactic Notation "efeed" constr(H) "using" tactic3(tac) :=
-- 
GitLab