diff --git a/iris/si_logic/siprop.v b/iris/si_logic/siprop.v
index d4e4b09eaf26cf5c95f8e7400362590a05eefae2..5361f62d2bca051c28b083c9311cafaf5fcbd1b2 100644
--- a/iris/si_logic/siprop.v
+++ b/iris/si_logic/siprop.v
@@ -130,8 +130,7 @@ Ltac unseal := rewrite !unseal_eqs /=.
 Section primitive.
 Local Arguments siProp_holds !_ _ /.
 
-Notation "P ⊢ Q" := (siProp_entails P Q)
-  (at level 99, Q at level 200, right associativity).
+Notation "P ⊢ Q" := (siProp_entails P Q).
 Notation "'True'" := (siProp_pure True) : siProp_scope.
 Notation "'False'" := (siProp_pure False) : siProp_scope.
 Notation "'⌜' φ '⌝'" := (siProp_pure φ%type%stdpp) : siProp_scope.
diff --git a/tests/proofmode.v b/tests/proofmode.v
index b679d03e14ae48a0eba5a29687fb1a936b20cb4a..8ad3f6da4b95f11a1f86e15748228e9556d8b504 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -865,7 +865,7 @@ Lemma test_specialize_intuitionistic P Q :
   □ P -∗ □ (P -∗ Q) -∗ □ Q.
 Proof. iIntros "#HP #HQ". iSpecialize ("HQ" with "HP"). done. Qed.
 
-Lemma test_iEval x y : ⌜ (y + x)%nat = 1 ⌝ -∗ ⌜ S (x + y) = 2%nat ⌝ : PROP.
+Lemma test_iEval x y : ⌜ (y + x)%nat = 1 ⌝ ⊢@{PROP} ⌜ S (x + y) = 2%nat ⌝.
 Proof.
   iIntros (H).
   iEval (rewrite (Nat.add_comm x y) // H).
@@ -880,21 +880,21 @@ Proof.
 Qed.
 
 Check "test_iSimpl_in".
-Lemma test_iSimpl_in x y : ⌜ (3 + x)%nat = y ⌝ -∗ ⌜ S (S (S x)) = y ⌝ : PROP.
+Lemma test_iSimpl_in x y : ⌜ (3 + x)%nat = y ⌝ ⊢@{PROP} ⌜ S (S (S x)) = y ⌝.
 Proof. iIntros "H". iSimpl in "H". Show. done. Qed.
 
 Lemma test_iSimpl_in_2 x y z :
-  ⌜ (3 + x)%nat = y ⌝ -∗ ⌜ (1 + y)%nat = z ⌝ -∗
-  ⌜ S (S (S x)) = y ⌝ : PROP.
+  ⌜ (3 + x)%nat = y ⌝ ⊢@{PROP} ⌜ (1 + y)%nat = z ⌝ -∗
+  ⌜ S (S (S x)) = y ⌝.
 Proof. iIntros "H1 H2". iSimpl in "H1 H2". Show. done. Qed.
 
 Lemma test_iSimpl_in3 x y z :
-  ⌜ (3 + x)%nat = y ⌝ -∗ ⌜ (1 + y)%nat = z ⌝ -∗
-  ⌜ S (S (S x)) = y ⌝ : PROP.
+  ⌜ (3 + x)%nat = y ⌝ ⊢@{PROP} ⌜ (1 + y)%nat = z ⌝ -∗
+  ⌜ S (S (S x)) = y ⌝.
 Proof. iIntros "#H1 H2". iSimpl in "#". Show. done. Qed.
 
 Check "test_iSimpl_in4".
-Lemma test_iSimpl_in4 x y : ⌜ (3 + x)%nat = y ⌝ -∗ ⌜ S (S (S x)) = y ⌝ : PROP.
+Lemma test_iSimpl_in4 x y : ⌜ (3 + x)%nat = y ⌝ ⊢@{PROP} ⌜ S (S (S x)) = y ⌝.
 Proof. iIntros "H". Fail iSimpl in "%". by iSimpl in "H". Qed.
 
 Check "test_iRename".
diff --git a/tests/proofmode_monpred.v b/tests/proofmode_monpred.v
index b9da25e4290bf2a2d49e07f604fbde86c6544883..25b7fe1977c75c6e75cf4e4be9710e1ef9991f70 100644
--- a/tests/proofmode_monpred.v
+++ b/tests/proofmode_monpred.v
@@ -67,7 +67,7 @@ Section tests.
     iStartProof. iIntros (n) "$".
   Qed.
 
-  Lemma test_embed_wand (P Q : PROP) : (⎡P⎤ -∗ ⎡Q⎤) -∗ ⎡P -∗ Q⎤ : monPred.
+  Lemma test_embed_wand (P Q : PROP) : (⎡P⎤ -∗ ⎡Q⎤) ⊢@{monPredI} ⎡P -∗ Q⎤.
   Proof.
     iIntros "H HP". by iApply "H".
   Qed.