diff --git a/tests/proofmode.ref b/tests/proofmode.ref
index a3d7a44daa111266a551e9491dae681c28eceef3..5d7abf860c800190ca3cded07aee2e382187eb30 100644
--- a/tests/proofmode.ref
+++ b/tests/proofmode.ref
@@ -74,6 +74,17 @@ Tactic failure: iSpecialize: cannot instantiate (⌜φ⌝ → P -∗ False)%I wi
   --------------------------------------∗
   â–·^(S n + S m) emp
   
+"test_iSimpl_in"
+     : string
+1 subgoal
+  
+  PROP : sbi
+  x, y : nat
+  ============================
+  "H" : ⌜S (S (S x)) = y⌝
+  --------------------------------------∗
+  ⌜S (S (S x)) = y⌝
+  
 "test_iFrame_later_1"
      : string
 1 subgoal
diff --git a/tests/proofmode.v b/tests/proofmode.v
index b71cbbf74b5972594d4ebfc60ab3b607eab47b40..d395d97ab31f45d739e48f92f79b27971cbbb7a8 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -412,6 +412,10 @@ Proof.
   done.
 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.
+
 Lemma test_iIntros_pure_neg : (⌜ ¬False ⌝ : PROP)%I.
 Proof. by iIntros (?). Qed.
 
diff --git a/theories/proofmode/ltac_tactics.v b/theories/proofmode/ltac_tactics.v
index c5d25de8f85fc0ace48aa719b73bc42e08fceb78..837f91c710fb5c37f077267871e0b5f052bb2152 100644
--- a/theories/proofmode/ltac_tactics.v
+++ b/theories/proofmode/ltac_tactics.v
@@ -119,8 +119,8 @@ Tactic Notation "iEval" tactic(t) "in" constr(H) :=
     |pm_reflexivity
     |].
 
-Tactic Notation "iSimpl" := iEval simpl.
-Tactic Notation "iSimpl" "in" constr(H) := iEval simpl in H.
+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: