From ac310b6a64e828ed86ba6dedf080aa5fcf86ab18 Mon Sep 17 00:00:00 2001
From: Gregory Malecha <gregory@bedrocksystems.com>
Date: Wed, 6 Apr 2022 22:22:04 -0400
Subject: [PATCH] Minor notation cleanup to avoid casts.

---
 iris/si_logic/siprop.v    |  3 +--
 tests/proofmode.v         | 14 +++++++-------
 tests/proofmode_monpred.v |  2 +-
 3 files changed, 9 insertions(+), 10 deletions(-)

diff --git a/iris/si_logic/siprop.v b/iris/si_logic/siprop.v
index d4e4b09ea..5361f62d2 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 b679d03e1..8ad3f6da4 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 b9da25e42..25b7fe197 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.
-- 
GitLab