reserve embedding notation as well

f31c5028 · Ralf Jung · 3d261c32 · f31c5028
Commit f31c5028 authored May 31, 2018 by Ralf Jung
Hide whitespace changes
Inline Side-by-side

Showing with 2 additions and 0 deletions

theories/bi/notation.v theories/bi/notation.v +2 -0

No files found.
--- 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,