add mk_evar tactic (to replace Coq's strange evar tactic) and use it

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.
 

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)

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] |- _ =>

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) :=