From f31c502863e0f0cb8eabb2d20ed5bf00bb7cce0c Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 31 May 2018 12:18:54 +0200
Subject: [PATCH] reserve embedding notation as well

---
 theories/bi/notation.v | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/theories/bi/notation.v b/theories/bi/notation.v
index 9a2a3656a..5322e6d71 100644
--- a/theories/bi/notation.v
+++ b/theories/bi/notation.v
@@ -14,6 +14,8 @@ Reserved Notation "'⌜' φ '⌝'" (at level 1, φ at level 200, format "⌜ φ
 Reserved Notation "P ∗ Q" (at level 80, right associativity).
 Reserved Notation "P -∗ Q" (at level 99, Q at level 200, right associativity).
 
+Reserved Notation "⎡ P ⎤".
+
 (** Modalities *)
 Reserved Notation "'<pers>' P" (at level 20, right associativity).
 Reserved Notation "'<pers>?' p P" (at level 20, p at level 9, P at level 20,
-- 
GitLab