From 3d261c32b804676cf16345340b8cc3f2026ace64 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 31 May 2018 12:12:35 +0200
Subject: [PATCH] also reserve monPred modalities

---
 theories/bi/monpred.v  | 4 ++--
 theories/bi/notation.v | 3 +++
 2 files changed, 5 insertions(+), 2 deletions(-)

diff --git a/theories/bi/monpred.v b/theories/bi/monpred.v
index e3191ffbf..0a01f4e0d 100644
--- a/theories/bi/monpred.v
+++ b/theories/bi/monpred.v
@@ -214,8 +214,8 @@ End Bi.
 
 Arguments monPred_objectively {_ _} _%I.
 Arguments monPred_subjectively {_ _} _%I.
-Notation "'<obj>' P" := (monPred_objectively P) (at level 20, right associativity) : bi_scope.
-Notation "'<subj>' P" := (monPred_subjectively P) (at level 20, right associativity) : bi_scope.
+Notation "'<obj>' P" := (monPred_objectively P) : bi_scope.
+Notation "'<subj>' P" := (monPred_subjectively P) : bi_scope.
 
 Section Sbi.
 Context {I : biIndex} {PROP : sbi}.
diff --git a/theories/bi/notation.v b/theories/bi/notation.v
index 586b5d2a1..9a2a3656a 100644
--- a/theories/bi/notation.v
+++ b/theories/bi/notation.v
@@ -43,6 +43,9 @@ Reserved Notation "â–  P" (at level 20, right associativity).
 Reserved Notation "â– ? p P" (at level 20, p at level 9, P at level 20,
    right associativity, format "â– ? p  P").
 
+Reserved Notation "'<obj>' P" (at level 20, right associativity).
+Reserved Notation "'<subj>' P" (at level 20, right associativity).
+
 (** Update modalities *)
 Reserved Notation "|==> Q" (at level 99, Q at level 200, format "|==>  Q").
 Reserved Notation "P ==∗ Q" (at level 99, Q at level 200, format "P  ==∗  Q").
-- 
GitLab