diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index 6295991ceaaad50616f9028b10a2ae9b00f1e3c5..1ed4cf3b0e8ca144cd6f3c1eaa3c6c3b16581821 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 eca07dc6797fb96910b149f9e7beb37c04cc7801..bb799aba3c7e3a3cad561b4a05986617e7d01960 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 0fd7dfaae60935620c14e3f221f9b46fb23ca92a..abdbf6f9f3b6e9847ca256fd2b38b785b9d6b237 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 39543e5f097147d56fba9df46c77d4ee212dd6f0..d3910a89c7e524253793f239617aa8d8015b64d7 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) :=