From b3af10b3156112aa6b76e1489e5c3a2cc458c11a Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 5 Apr 2018 13:57:45 +0200
Subject: [PATCH] =?UTF-8?q?make=20the=20annotated=20notations=20only=20par?=
 =?UTF-8?q?sing;=20add=20annotated=20versions=20of=20the=20curried=20forms?=
 =?UTF-8?q?=20(=E2=8A=A2)=20and=20(=E2=8A=A3=E2=8A=A2)?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 theories/bi/interface.v | 10 ++++++----
 1 file changed, 6 insertions(+), 4 deletions(-)

diff --git a/theories/bi/interface.v b/theories/bi/interface.v
index 6c69a2678..3a1d4b698 100644
--- a/theories/bi/interface.v
+++ b/theories/bi/interface.v
@@ -2,9 +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).
 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 "P '⊣⊢@{' PROP } Q" (at level 95, no associativity).
 Reserved Notation "'emp'".
 Reserved Notation "'⌜' φ '⌝'" (at level 1, φ at level 200, format "⌜ φ ⌝").
 Reserved Notation "P ∗ Q" (at level 80, right associativity).
@@ -268,12 +268,14 @@ 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) (only parsing) : stdpp_scope.
 Notation "(⊢)" := bi_entails (only parsing) : stdpp_scope.
+Notation "(⊢@{ PROP })" := (bi_entails (PROP:=PROP)) (only parsing) : 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 "P ⊣⊢@{ PROP } Q" := (equiv (A:=bi_car PROP) P%I Q%I) (only parsing) : stdpp_scope.
 Notation "(⊣⊢)" := (equiv (A:=bi_car _)) (only parsing) : stdpp_scope.
+Notation "(⊣⊢@{ PROP })" := (equiv (A:=bi_car PROP)) (only parsing) : stdpp_scope.
 
 Notation "P -∗ Q" := (P ⊢ Q) : stdpp_scope.
 
-- 
GitLab