From 75e30fd58e2e69ce33643a27e844452e573e4ac2 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 5 Apr 2018 17:51:15 +0200
Subject: [PATCH] fix notation conflict

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

diff --git a/theories/bi/interface.v b/theories/bi/interface.v
index 3a1d4b698..b90fdfd99 100644
--- a/theories/bi/interface.v
+++ b/theories/bi/interface.v
@@ -3,8 +3,10 @@ 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).
+Reserved Notation "('⊢@{' PROP } )" (at level 99).
 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 "'emp'".
 Reserved Notation "'⌜' φ '⌝'" (at level 1, φ at level 200, format "⌜ φ ⌝").
 Reserved Notation "P ∗ Q" (at level 80, right associativity).
@@ -270,12 +272,12 @@ 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 "(⊢)" := 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 "(⊣⊢)" := (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.
 
-- 
GitLab