From 0c0f84bc0b327e2c464530936d67ee21473b445e Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 24 Feb 2020 09:51:51 +0100
Subject: [PATCH] Fix discrepancies in bi notations.

Thanks to @Blaisorblade, based on
https://gitlab.mpi-sws.org/Blaisorblade/iris-coq/commit/0739608d32272ca5679bf504a569b3ddd50c7b29,
but applied to similar notations too.
---
 theories/bi/interface.v | 8 ++++----
 theories/bi/notation.v  | 7 +++++--
 2 files changed, 9 insertions(+), 6 deletions(-)

diff --git a/theories/bi/interface.v b/theories/bi/interface.v
index 4eb80f6c7..fd09f4c2f 100644
--- a/theories/bi/interface.v
+++ b/theories/bi/interface.v
@@ -260,14 +260,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) (only parsing) : 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 "('⊢@{' 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) (only parsing) : 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 "('⊣⊢@{' PROP } )" := (equiv (A:=bi_car PROP)) (only parsing) : stdpp_scope.
 
 Notation "P -∗ Q" := (P ⊢ Q) : stdpp_scope.
 
diff --git a/theories/bi/notation.v b/theories/bi/notation.v
index 953448198..8b268c974 100644
--- a/theories/bi/notation.v
+++ b/theories/bi/notation.v
@@ -3,10 +3,13 @@
 (** Turnstiles *)
 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).
-Reserved Notation "('⊢@{' PROP } )" (at level 99).
+Reserved Notation "(⊢)".
+Reserved Notation "('⊢@{' PROP } )".
+
 Reserved Notation "P ⊣⊢ Q" (at level 95, no associativity).
 Reserved Notation "P '⊣⊢@{' PROP } Q" (at level 95, no associativity).
-Reserved Notation "('⊣⊢@{' PROP } )" (at level 95).
+Reserved Notation "(⊣⊢)".
+Reserved Notation "('⊣⊢@{' PROP } )".
 
 (** BI connectives *)
 Reserved Notation "'emp'".
-- 
GitLab