From 0739608d32272ca5679bf504a569b3ddd50c7b29 Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <p.giarrusso@gmail.com>
Date: Sun, 23 Feb 2020 19:59:20 +0100
Subject: [PATCH] Fix parsing issue

This notation disagreed with the variant declared in `notation.v`; that was the
whole problem. Beware the resulting code is still not specified to work.
---
 theories/bi/embedding.v | 2 +-
 theories/bi/interface.v | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/theories/bi/embedding.v b/theories/bi/embedding.v
index 3ddb3479a..3eaa91784 100644
--- a/theories/bi/embedding.v
+++ b/theories/bi/embedding.v
@@ -84,7 +84,7 @@ Section embed_laws.
   Proof. eapply bi_embed_mixin_ne, bi_embed_mixin. Qed.
   Global Instance embed_mono : Proper ((⊢) ==> (⊢)) embed.
   Proof. eapply bi_embed_mixin_mono, bi_embed_mixin. Qed.
-  Lemma embed_emp_valid_inj P : ( ⊢@{PROP2} ⎡P⎤) → ⊢ P.
+  Lemma embed_emp_valid_inj P : (⊢@{PROP2} ⎡P⎤) → ⊢ P.
   Proof. eapply bi_embed_mixin_emp_valid_inj, bi_embed_mixin. Qed.
   Lemma embed_emp_2 : emp ⊢ ⎡emp⎤.
   Proof. eapply bi_embed_mixin_emp_2, bi_embed_mixin. Qed.
diff --git a/theories/bi/interface.v b/theories/bi/interface.v
index f233be208..9fb540cff 100644
--- a/theories/bi/interface.v
+++ b/theories/bi/interface.v
@@ -262,7 +262,7 @@ 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.
-- 
GitLab