diff --git a/tests/proofmode.ref b/tests/proofmode.ref
index e1ab0ee889e8ae99abeb59db2dad4ae123432db7..b50195bf3eedabe4b237f20955372c8a7631ee1b 100644
--- a/tests/proofmode.ref
+++ b/tests/proofmode.ref
@@ -126,7 +126,7 @@ Tactic failure: iSpecialize: cannot instantiate (⌜φ⌝ → P -∗ False)%I wi
      : string
 The command has indeed failed with message:
 In nested Ltac calls to "iSimpl in (constr)",
-"iEval (tactic) in (constr)" and "<iris.proofmode.ltac_tactics.iEval_go>",
+"iEval (tactic3) in (constr)" and "<iris.proofmode.ltac_tactics.iEval_go>",
 last call failed.
 Tactic failure: iEval: %: unsupported selection pattern.
 "test_iFrame_later_1"
diff --git a/tests/proofmode.v b/tests/proofmode.v
index 515cb9dbd80f741b8193195789d066dd882a0a8e..f1b43337b65f11f4110fb8c0de3429d0ef03bb23 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -480,6 +480,13 @@ Proof.
   done.
 Qed.
 
+Lemma test_iEval_precedence : True ⊢ True : PROP.
+Proof.
+  iIntros.
+  (* Ensure that in [iEval (a); b], b is not parsed as part of the argument of [iEval]. *)
+  iEval (rewrite /=); iPureIntro; exact I.
+Qed.
+
 Check "test_iSimpl_in".
 Lemma test_iSimpl_in x y : ⌜ (3 + x)%nat = y ⌝ -∗ ⌜ S (S (S x)) = y ⌝ : PROP.
 Proof. iIntros "H". iSimpl in "H". Show. done. Qed.
diff --git a/theories/proofmode/ltac_tactics.v b/theories/proofmode/ltac_tactics.v
index dff46653bee6b1936ba82cf24161028370356167..2d055b316e33133b587bcad2b8dad9fd511abb53 100644
--- a/theories/proofmode/ltac_tactics.v
+++ b/theories/proofmode/ltac_tactics.v
@@ -195,7 +195,7 @@ Tactic Notation "iClear" "(" ident_list(xs) ")" constr(Hs) :=
   iClear Hs; clear xs.
 
 (** ** Simplification *)
-Tactic Notation "iEval" tactic(t) :=
+Tactic Notation "iEval" tactic3(t) :=
   iStartProof;
   eapply tac_eval;
     [let x := fresh in intros x; t; unfold x; reflexivity
@@ -212,7 +212,7 @@ Local Ltac iEval_go t Hs :=
       |pm_reduce; iEval_go t Hs]
   end.
 
-Tactic Notation "iEval" tactic(t) "in" constr(Hs) :=
+Tactic Notation "iEval" tactic3(t) "in" constr(Hs) :=
   iStartProof; let Hs := iElaborateSelPat Hs in iEval_go t Hs.
 
 Tactic Notation "iSimpl" := iEval (simpl).