diff --git a/theories/bi/monpred.v b/theories/bi/monpred.v
index e3191ffbf81bdcef0a705120c8b3180a7ab2aff9..0a01f4e0d7a5b014ab134772c2630efc1c2aef01 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 586b5d2a191ad752adf07afae52200d3a606bf7a..9a2a3656a129a247b6e7327cb64a67b7fda7e7a7 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").