From e53c8a39b29c366f956dde0b8da7443356159c1a Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 5 Apr 2018 11:02:50 +0200
Subject: [PATCH] add '@' to type ascription notation for disambiguation

---
 theories/bi/big_op.v           |  2 +-
 theories/bi/derived_laws_bi.v  |  4 ++--
 theories/bi/derived_laws_sbi.v |  4 ++--
 theories/bi/embedding.v        |  6 +++---
 theories/bi/interface.v        | 26 +++++++++++++-------------
 theories/bi/monpred.v          |  2 +-
 theories/bi/plainly.v          | 10 +++++-----
 7 files changed, 27 insertions(+), 27 deletions(-)

diff --git a/theories/bi/big_op.v b/theories/bi/big_op.v
index b583279fd..477105c84 100644
--- a/theories/bi/big_op.v
+++ b/theories/bi/big_op.v
@@ -89,7 +89,7 @@ Section sep_list.
     Proper (Forall2 (⊢) ==> (⊢)) (big_opL (@bi_sep M) (λ _ P, P)).
   Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed.
 
-  Lemma big_sepL_emp l : ([∗ list] k↦y ∈ l, emp) ⊣⊢{PROP} emp.
+  Lemma big_sepL_emp l : ([∗ list] k↦y ∈ l, emp) ⊣⊢@{PROP} emp.
   Proof. by rewrite big_opL_unit. Qed.
 
   Lemma big_sepL_lookup_acc Φ l i x :
diff --git a/theories/bi/derived_laws_bi.v b/theories/bi/derived_laws_bi.v
index 41428b317..0143774a7 100644
--- a/theories/bi/derived_laws_bi.v
+++ b/theories/bi/derived_laws_bi.v
@@ -21,8 +21,8 @@ Implicit Types A : Type.
 Hint Extern 100 (NonExpansive _) => solve_proper.
 
 (* Force implicit argument PROP *)
-Notation "P ⊢ Q" := (P ⊢{PROP} Q).
-Notation "P ⊣⊢ Q" := (P ⊣⊢{PROP} Q).
+Notation "P ⊢ Q" := (P ⊢@{PROP} Q).
+Notation "P ⊣⊢ Q" := (P ⊣⊢@{PROP} Q).
 
 (* Derived stuff about the entailment *)
 Global Instance entails_anti_sym : AntiSymm (⊣⊢) (@bi_entails PROP).
diff --git a/theories/bi/derived_laws_sbi.v b/theories/bi/derived_laws_sbi.v
index 241f27eea..147a2f739 100644
--- a/theories/bi/derived_laws_sbi.v
+++ b/theories/bi/derived_laws_sbi.v
@@ -13,8 +13,8 @@ Implicit Types Ps : list PROP.
 Implicit Types A : Type.
 
 (* Force implicit argument PROP *)
-Notation "P ⊢ Q" := (P ⊢{PROP} Q).
-Notation "P ⊣⊢ Q" := (P ⊣⊢{PROP} Q).
+Notation "P ⊢ Q" := (P ⊢@{PROP} Q).
+Notation "P ⊣⊢ Q" := (P ⊣⊢@{PROP} Q).
 
 Hint Resolve or_elim or_intro_l' or_intro_r' True_intro False_elim.
 Hint Resolve and_elim_l' and_elim_r' and_intro forall_intro.
diff --git a/theories/bi/embedding.v b/theories/bi/embedding.v
index 810d97e9d..ee071f187 100644
--- a/theories/bi/embedding.v
+++ b/theories/bi/embedding.v
@@ -36,21 +36,21 @@ Arguments bi_embed_embed : simpl never.
 Class SbiEmbed (PROP1 PROP2 : sbi) `{BiEmbed PROP1 PROP2} := {
   embed_internal_eq_1 (A : ofeT) (x y : A) : ⎡x ≡ y⎤ ⊢ x ≡ y;
   embed_later P : ⎡▷ P⎤ ⊣⊢ ▷ ⎡P⎤;
-  embed_interal_inj (PROP' : sbi) (P Q : PROP1) : ⎡P⎤ ≡ ⎡Q⎤ ⊢{PROP'} (P ≡ Q);
+  embed_interal_inj (PROP' : sbi) (P Q : PROP1) : ⎡P⎤ ≡ ⎡Q⎤ ⊢@{PROP'} (P ≡ Q);
 }.
 Hint Mode SbiEmbed ! - - : typeclass_instances.
 Hint Mode SbiEmbed - ! - : typeclass_instances.
 
 Class BiEmbedBUpd (PROP1 PROP2 : bi)
       `{BiEmbed PROP1 PROP2, BiBUpd PROP1, BiBUpd PROP2} := {
-  embed_bupd  P : ⎡|==> P⎤ ⊣⊢{PROP2} |==> ⎡P⎤
+  embed_bupd  P : ⎡|==> P⎤ ⊣⊢@{PROP2} |==> ⎡P⎤
 }.
 Hint Mode BiEmbedBUpd - ! - - - : typeclass_instances.
 Hint Mode BiEmbedBUpd ! - - - - : typeclass_instances.
 
 Class BiEmbedFUpd (PROP1 PROP2 : sbi)
       `{BiEmbed PROP1 PROP2, BiFUpd PROP1, BiFUpd PROP2} := {
-  embed_fupd E1 E2 P : ⎡|={E1,E2}=> P⎤ ⊣⊢{PROP2} |={E1,E2}=> ⎡P⎤
+  embed_fupd E1 E2 P : ⎡|={E1,E2}=> P⎤ ⊣⊢@{PROP2} |={E1,E2}=> ⎡P⎤
 }.
 Hint Mode BiEmbedFUpd - ! - - - : typeclass_instances.
 Hint Mode BiEmbedFUpd ! - - - - : typeclass_instances.
diff --git a/theories/bi/interface.v b/theories/bi/interface.v
index c1820e524..6c69a2678 100644
--- a/theories/bi/interface.v
+++ b/theories/bi/interface.v
@@ -2,7 +2,9 @@ From iris.algebra Require Export ofe.
 Set Primitive Projections.
 
 Reserved Notation "P ⊢ Q" (at level 99, Q at level 200, right associativity).
-Reserved Notation "P ⊢{ PROP } Q" (at level 99, Q at level 200, right associativity, format "P  '⊢{' PROP '}'  Q").
+Reserved Notation "P '⊢@{' PROP } Q" (at level 99, Q at level 200, right associativity, format "P  '⊢@{' PROP '}'  Q").
+Reserved Notation "P ⊣⊢ Q" (at level 95, no associativity).
+Reserved Notation "P '⊣⊢@{' PROP } Q" (at level 95, no associativity, format "P  '⊣⊢@{' PROP '}'  Q").
 Reserved Notation "'emp'".
 Reserved Notation "'⌜' φ '⌝'" (at level 1, φ at level 200, format "⌜ φ ⌝").
 Reserved Notation "P ∗ Q" (at level 80, right associativity).
@@ -266,13 +268,11 @@ Instance bi_rewrite_relation (PROP : bi) : RewriteRelation (@bi_entails PROP).
 Instance bi_inhabited {PROP : bi} : Inhabited PROP := populate (bi_pure True).
 
 Notation "P ⊢ Q" := (bi_entails P%I Q%I) : stdpp_scope.
-Notation "P ⊢{ PROP } Q" := (bi_entails (PROP:=PROP) P%I Q%I) : stdpp_scope.
+Notation "P ⊢@{ PROP } Q" := (bi_entails (PROP:=PROP) P%I Q%I) : stdpp_scope.
 Notation "(⊢)" := bi_entails (only parsing) : stdpp_scope.
 
-Notation "P ⊣⊢ Q" := (equiv (A:=bi_car _) P%I Q%I)
-  (at level 95, no associativity) : stdpp_scope.
-Notation "P ⊣⊢{ PROP } Q" := (equiv (A:=bi_car PROP) P%I Q%I)
-  (at level 95, no associativity) : stdpp_scope.
+Notation "P ⊣⊢ Q" := (equiv (A:=bi_car _) P%I Q%I) : stdpp_scope.
+Notation "P ⊣⊢@{ PROP } Q" := (equiv (A:=bi_car PROP) P%I Q%I) : stdpp_scope.
 Notation "(⊣⊢)" := (equiv (A:=bi_car _)) (only parsing) : stdpp_scope.
 
 Notation "P -∗ Q" := (P ⊢ Q) : stdpp_scope.
@@ -344,7 +344,7 @@ Lemma pure_intro P (φ : Prop) : φ → P ⊢ ⌜ φ ⌝.
 Proof. eapply bi_mixin_pure_intro, bi_bi_mixin. Qed.
 Lemma pure_elim' (φ : Prop) P : (φ → True ⊢ P) → ⌜ φ ⌝ ⊢ P.
 Proof. eapply bi_mixin_pure_elim', bi_bi_mixin. Qed.
-Lemma pure_forall_2 {A} (φ : A → Prop) : (∀ a, ⌜ φ a ⌝) ⊢{PROP} ⌜ ∀ a, φ a ⌝.
+Lemma pure_forall_2 {A} (φ : A → Prop) : (∀ a, ⌜ φ a ⌝) ⊢@{PROP} ⌜ ∀ a, φ a ⌝.
 Proof. eapply bi_mixin_pure_forall_2, bi_bi_mixin. Qed.
 
 Lemma and_elim_l P Q : P ∧ Q ⊢ P.
@@ -398,7 +398,7 @@ Proof. eapply bi_mixin_persistently_mono, bi_bi_mixin. Qed.
 Lemma persistently_idemp_2 P : <pers> P ⊢ <pers> <pers> P.
 Proof. eapply bi_mixin_persistently_idemp_2, bi_bi_mixin. Qed.
 
-Lemma persistently_emp_2 : emp ⊢{PROP} <pers> emp.
+Lemma persistently_emp_2 : emp ⊢@{PROP} <pers> emp.
 Proof. eapply bi_mixin_persistently_emp_2, bi_bi_mixin. Qed.
 
 Lemma persistently_forall_2 {A} (Ψ : A → PROP) :
@@ -430,22 +430,22 @@ Lemma internal_eq_rewrite {A : ofeT} a b (Ψ : A → PROP) :
 Proof. eapply sbi_mixin_internal_eq_rewrite, sbi_sbi_mixin. Qed.
 
 Lemma fun_ext {A} {B : A → ofeT} (f g : ofe_fun B) :
-  (∀ x, f x ≡ g x) ⊢{PROP} f ≡ g.
+  (∀ x, f x ≡ g x) ⊢@{PROP} f ≡ g.
 Proof. eapply sbi_mixin_fun_ext, sbi_sbi_mixin. Qed.
 Lemma sig_eq {A : ofeT} (P : A → Prop) (x y : sig P) :
-  `x ≡ `y ⊢{PROP} x ≡ y.
+  `x ≡ `y ⊢@{PROP} x ≡ y.
 Proof. eapply sbi_mixin_sig_eq, sbi_sbi_mixin. Qed.
 Lemma discrete_eq_1 {A : ofeT} (a b : A) :
-  Discrete a → a ≡ b ⊢{PROP} ⌜a ≡ b⌝.
+  Discrete a → a ≡ b ⊢@{PROP} ⌜a ≡ b⌝.
 Proof. eapply sbi_mixin_discrete_eq_1, sbi_sbi_mixin. Qed.
 
 (* Later *)
 Global Instance later_contractive : Contractive (@sbi_later PROP).
 Proof. eapply sbi_mixin_later_contractive, sbi_sbi_mixin. Qed.
 
-Lemma later_eq_1 {A : ofeT} (x y : A) : Next x ≡ Next y ⊢{PROP} ▷ (x ≡ y).
+Lemma later_eq_1 {A : ofeT} (x y : A) : Next x ≡ Next y ⊢@{PROP} ▷ (x ≡ y).
 Proof. eapply sbi_mixin_later_eq_1, sbi_sbi_mixin. Qed.
-Lemma later_eq_2 {A : ofeT} (x y : A) : ▷ (x ≡ y) ⊢{PROP} Next x ≡ Next y.
+Lemma later_eq_2 {A : ofeT} (x y : A) : ▷ (x ≡ y) ⊢@{PROP} Next x ≡ Next y.
 Proof. eapply sbi_mixin_later_eq_2, sbi_sbi_mixin. Qed.
 
 Lemma later_mono P Q : (P ⊢ Q) → ▷ P ⊢ ▷ Q.
diff --git a/theories/bi/monpred.v b/theories/bi/monpred.v
index 6cd63ca93..4de962442 100644
--- a/theories/bi/monpred.v
+++ b/theories/bi/monpred.v
@@ -823,7 +823,7 @@ Lemma monPred_at_except_0 i P : (◇ P) i ⊣⊢ ◇ P i.
 Proof. by unseal. Qed.
 
 Lemma monPred_equivI {PROP' : sbi} P Q :
-  P ≡ Q ⊣⊢{PROP'} ∀ i, P i ≡ Q i.
+  P ≡ Q ⊣⊢@{PROP'} ∀ i, P i ≡ Q i.
 Proof.
   apply bi.equiv_spec. split.
   - apply bi.forall_intro=>?. apply (bi.f_equiv (flip monPred_at _)).
diff --git a/theories/bi/plainly.v b/theories/bi/plainly.v
index e6ed67b30..7f15fee34 100644
--- a/theories/bi/plainly.v
+++ b/theories/bi/plainly.v
@@ -161,7 +161,7 @@ Proof. apply (anti_symm _); auto using plainly_idemp_1, plainly_idemp_2. Qed.
 Lemma plainly_intro' P Q : (■ P ⊢ Q) → ■ P ⊢ ■ Q.
 Proof. intros <-. apply plainly_idemp_2. Qed.
 
-Lemma plainly_pure φ : ■ ⌜φ⌝ ⊣⊢{PROP} ⌜φ⌝.
+Lemma plainly_pure φ : ■ ⌜φ⌝ ⊣⊢@{PROP} ⌜φ⌝.
 Proof.
   apply (anti_symm _); auto.
   - by rewrite plainly_elim_persistently persistently_pure.
@@ -204,7 +204,7 @@ Proof. by rewrite -{1}(left_id emp%I _ Q%I) plainly_and_sep_assoc and_elim_l. Qe
 Lemma plainly_and_sep_r_1 P Q : P ∧ ■ Q ⊢ P ∗ ■ Q.
 Proof. by rewrite !(comm _ P) plainly_and_sep_l_1. Qed.
 
-Lemma plainly_True_emp : ■ True ⊣⊢{PROP} ■ emp.
+Lemma plainly_True_emp : ■ True ⊣⊢@{PROP} ■ emp.
 Proof. apply (anti_symm _); eauto using plainly_mono, plainly_emp_intro. Qed.
 Lemma plainly_and_sep P Q : ■ (P ∧ Q) ⊢ ■ (P ∗ Q).
 Proof.
@@ -273,7 +273,7 @@ Proof. rewrite -!impl_wand_affinely_plainly. apply plainly_impl_plainly. Qed.
 Section plainly_affine_bi.
   Context `{BiAffine PROP}.
 
-  Lemma plainly_emp : ■ emp ⊣⊢{PROP} emp.
+  Lemma plainly_emp : ■ emp ⊣⊢@{PROP} emp.
   Proof. by rewrite -!True_emp plainly_pure. Qed.
 
   Lemma plainly_and_sep_l P Q : ■ P ∧ Q ⊣⊢ ■ P ∗ Q.
@@ -311,7 +311,7 @@ Proof. solve_proper. Qed.
 Lemma plainly_if_mono p P Q : (P ⊢ Q) → ■?p P ⊢ ■?p Q.
 Proof. by intros ->. Qed.
 
-Lemma plainly_if_pure p φ : ■?p ⌜φ⌝ ⊣⊢{PROP} ⌜φ⌝.
+Lemma plainly_if_pure p φ : ■?p ⌜φ⌝ ⊣⊢@{PROP} ⌜φ⌝.
 Proof. destruct p; simpl; auto using plainly_pure. Qed.
 Lemma plainly_if_and p P Q : ■?p (P ∧ Q) ⊣⊢ ■?p P ∧ ■?p Q.
 Proof. destruct p; simpl; auto using plainly_and. Qed.
@@ -458,7 +458,7 @@ Global Instance from_option_plain {A} P (Ψ : A → PROP) (mx : option A) :
 Proof. destruct mx; apply _. Qed.
 
 (* Interaction with equality *)
-Lemma plainly_internal_eq {A:ofeT} (a b : A) : ■ (a ≡ b) ⊣⊢{PROP} a ≡ b.
+Lemma plainly_internal_eq {A:ofeT} (a b : A) : ■ (a ≡ b) ⊣⊢@{PROP} a ≡ b.
 Proof.
   apply (anti_symm (⊢)).
   { by rewrite plainly_elim. }
-- 
GitLab