diff --git a/theories/heap_lang/proofmode.v b/theories/heap_lang/proofmode.v
index 24a22025c75200f80494f1ad9b14b2c6c811a297..e8513242cbc9bb9fb336ecd051514a425a61a71d 100644
--- a/theories/heap_lang/proofmode.v
+++ b/theories/heap_lang/proofmode.v
@@ -6,18 +6,20 @@ Set Default Proof Using "Type".
 Import uPred.
 
 Lemma tac_wp_expr_eval `{heapG Σ} Δ s E Φ e e' :
-  e = e' →
+  (∀ (e'':=e'), e = e'') →
   envs_entails Δ (WP e' @ s; E {{ Φ }}) → envs_entails Δ (WP e @ s; E {{ Φ }}).
 Proof. by intros ->. Qed.
 Lemma tac_twp_expr_eval `{heapG Σ} Δ s E Φ e e' :
-  e = e' →
+  (∀ (e'':=e'), e = e'') →
   envs_entails Δ (WP e' @ s; E [{ Φ }]) → envs_entails Δ (WP e @ s; E [{ Φ }]).
 Proof. by intros ->. Qed.
 
 Tactic Notation "wp_expr_eval" tactic(t) :=
-  try iStartProof;
-  try (first [eapply tac_wp_expr_eval|eapply tac_twp_expr_eval];
-       [t; reflexivity|]).
+  try (
+    iStartProof;
+    first [eapply tac_wp_expr_eval|eapply tac_twp_expr_eval];
+      [let x := fresh in intros x; t; unfold x; reflexivity
+      |]).
 
 Ltac wp_expr_simpl := wp_expr_eval simpl.
 Ltac wp_expr_simpl_subst := wp_expr_eval simpl_subst.
diff --git a/theories/proofmode/coq_tactics.v b/theories/proofmode/coq_tactics.v
index ac28a1a1b9a0277ee281e51379b7bade677e0bc3..73503b3611dbdb3d934448a0e78dad1947260634 100644
--- a/theories/proofmode/coq_tactics.v
+++ b/theories/proofmode/coq_tactics.v
@@ -414,13 +414,15 @@ Qed.
 
 (** * Basic rules *)
 Lemma tac_eval Δ Q Q' :
-  (Q' ⊢ Q) →
+  (∀ (Q'':=Q'), Q'' ⊢ Q) → (* We introduce [Q''] as a let binding so that
+    tactics like `reflexivity` as called by [rewrite //] do not eagerly unify
+    it with [Q]. See [test_iEval] in [tests/proofmode]. *)
   envs_entails Δ Q' → envs_entails Δ Q.
 Proof. by intros <-. Qed.
 
 Lemma tac_eval_in Δ Δ' i p P P' Q :
   envs_lookup i Δ = Some (p, P) →
-  (P ⊢ P') →
+  (∀ (P'':=P'), P ⊢ P') →
   envs_simple_replace i p (Esnoc Enil i P') Δ  = Some Δ' →
   envs_entails Δ' Q → envs_entails Δ Q.
 Proof.
diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index 444ed40691734a69ca995244cd93c063e8a1fe1e..d09938c847034b490ae0c61e561976a7c0b55aeb 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -83,13 +83,14 @@ Ltac iStartProof :=
 (** * Simplification *)
 Tactic Notation "iEval" tactic(t) :=
   iStartProof;
-  eapply tac_eval; [t; reflexivity|].
+  eapply tac_eval;
+    [let x := fresh in intros x; t; unfold x; reflexivity|].
 
 Tactic Notation "iEval" tactic(t) "in" constr(H) :=
   iStartProof;
   eapply tac_eval_in with _ H _ _ _;
     [env_reflexivity || fail "iEval:" H "not found"
-    |t; reflexivity
+    |let x := fresh in intros x; t; unfold x; reflexivity
     |env_reflexivity
     |].
 
diff --git a/theories/tests/proofmode.v b/theories/tests/proofmode.v
index caaabaec9e0b9e4fd7088ed32ce6b69ae86df9a6..f257ff719c61eac5f285e58fc3742f39ebe02c6e 100644
--- a/theories/tests/proofmode.v
+++ b/theories/tests/proofmode.v
@@ -285,6 +285,13 @@ Proof. iIntros "H". iNext. by iNext. Qed.
 Lemma test_iNext_laterN_laterN P n1 n2 : ▷ ▷^n1 ▷^n2 P ⊢ ▷^n1 ▷^n2 ▷ P.
 Proof. iIntros "H". iNext. iNext. by iNext. Qed.
 
+Lemma test_iEval x y : ⌜ (y + x)%nat = 1 ⌝ -∗ ⌜ S (x + y) = 2%nat ⌝ : uPred M.
+Proof.
+  iIntros (H).
+  iEval (rewrite (Nat.add_comm x y) // H).
+  done.
+Qed.
+
 (* TODO: This test is broken in Coq 8.6. Should be restored once we drop Coq
 8.6 support. See also issue #108. *)
 (*