diff --git a/ProofMode.md b/ProofMode.md
index cc19fdf3d8368ba37d0654b94d7e772a3b5c4726..06ba8e1c82d4bba30dfc53127761313d423e5c16 100644
--- a/ProofMode.md
+++ b/ProofMode.md
@@ -150,11 +150,22 @@ Induction
   variables `x1 ... xn`, the hypotheses given by the selection pattern `selpat`,
   and the spatial context.
 
-Rewriting
----------
+Rewriting / simplification
+--------------------------
+
+- `iRewrite pm_trm` / `iRewrite pm_trm in "H"` : rewrite using an internal
+  equality in the proof mode goal / hypothesis `H`.
+- `iEval (tac)` / `iEval (tac) in H` : performs a tactic `tac` on the proof mode
+  goal / hypothesis `H`. The tactic `tac` should be a reduction or rewriting
+  tactic like `simpl`, `cbv`, `lazy`, `rewrite` or `setoid_rewrite`. The `iEval`
+  tactic is implemented by running `tac` on `?evar ⊢ P` / `P ⊢ ?evar` where `P`
+  is the proof goal / hypothesis `H`. After running `tac`, `?evar` is unified
+  with the resulting `P`, which in turn becomes the new proof mode goal /
+  hypothesis `H`.
+  Note that parentheses around `tac` are needed.
+- `iSimpl` / `iSimpl in H` : performs `simpl` on the proof mode goal /
+  hypothesis `H`. This is a shorthand for `iEval (simpl)`.
 
-- `iRewrite pm_trm` : rewrite an equality in the conclusion.
-- `iRewrite pm_trm in "H"` : rewrite an equality in the hypothesis `H`.
 
 Iris
 ----
diff --git a/theories/base_logic/lib/boxes.v b/theories/base_logic/lib/boxes.v
index cf8aff8a07e1225775e73eab7983b4532044d26f..52e4d2bd10607fb2ca0578374f4b4e0831086661 100644
--- a/theories/base_logic/lib/boxes.v
+++ b/theories/base_logic/lib/boxes.v
@@ -209,7 +209,7 @@ Lemma box_fill E f P :
 Proof.
   iIntros (?) "H HP"; iDestruct "H" as (Φ) "[#HeqP Hf]".
   iExists Φ; iSplitR; first by rewrite big_opM_fmap.
-  rewrite internal_eq_iff later_iff big_opM_commute.
+  iEval (rewrite internal_eq_iff later_iff big_opM_commute) in "HeqP".
   iDestruct ("HeqP" with "HP") as "HP".
   iCombine "Hf" "HP" as "Hf".
   rewrite -big_opM_opM big_opM_fmap; iApply (fupd_big_sepM _ _ f).
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 121102ce20fcf089cff9176cc4d5fb6f7220fce1..73503b3611dbdb3d934448a0e78dad1947260634 100644
--- a/theories/proofmode/coq_tactics.v
+++ b/theories/proofmode/coq_tactics.v
@@ -414,9 +414,22 @@ 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.
+Proof. by intros <-. Qed.
+
+Lemma tac_eval_in Δ Δ' i p P P' Q :
+  envs_lookup i Δ = Some (p, P) →
+  (∀ (P'':=P'), P ⊢ P') →
+  envs_simple_replace i p (Esnoc Enil i P') Δ  = Some Δ' →
+  envs_entails Δ' Q → envs_entails Δ Q.
+Proof.
+  rewrite /envs_entails. intros ? HP ? <-.
+  rewrite envs_simple_replace_sound //; simpl.
+  by rewrite HP right_id wand_elim_r.
+Qed.
 
 Lemma tac_assumption Δ i p P Q :
   envs_lookup i Δ = Some (p,P) → FromAssumption p P Q →
diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index 25e1a364bf56c7a05f8f66cdb71e223073554e63..d09938c847034b490ae0c61e561976a7c0b55aeb 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -82,10 +82,28 @@ Ltac iStartProof :=
 
 (** * Simplification *)
 Tactic Notation "iEval" tactic(t) :=
-  try iStartProof;
-  try (eapply tac_eval; [t; reflexivity|]).
+  iStartProof;
+  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"
+    |let x := fresh in intros x; t; unfold x; reflexivity
+    |env_reflexivity
+    |].
 
 Tactic Notation "iSimpl" := iEval simpl.
+Tactic Notation "iSimpl" "in" constr(H) := iEval simpl in H.
+
+(* It would be nice to also have an `iSsrRewrite`, however, for this we need to
+pass arguments to Ssreflect's `rewrite` like `/= foo /bar` in Ltac, see:
+
+  https://sympa.inria.fr/sympa/arc/coq-club/2018-01/msg00000.html
+
+PMP told me (= Robbert) in person that this is not possible today, but may be
+possible in Ltac2. *)
 
 (** * Context manipulation *)
 Tactic Notation "iRename" constr(H1) "into" constr(H2) :=
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. *)
 (*