Minor notation cleanup to avoid casts.

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.

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".

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.