diff --git a/docs/style_guide.md b/docs/style_guide.md
index 43c689e28db1f90b30c8e94d4ef39d5342956df0..64b848ac3529a01fa107b548a51a8383832c53cb 100644
--- a/docs/style_guide.md
+++ b/docs/style_guide.md
@@ -32,6 +32,21 @@ Typeclasses Opaque join_handle.
 This makes sure that the proof mode does not "look into" your definition when it
 is used by clients.
 
+## Notations
+
+Notations starting with `(` or `{` should be left at their default level (`0`),
+and inner subexpressions that are bracketed by delimiters should be left at
+their default level (`200`).
+
+Moreover, correct parsing of notations sometimes relies on Coq's automatic
+left-factoring, which can require coordinating levels of certain "conflicting"
+notations and their subexpressions. For instance, to disambiguate `(⊢@{ PROP })`
+and `(⊢@{ PROP } P)`, Coq must factor out a nonterminal for `⊢@{ PROP }`, but it
+can only do so if all occurrences of `⊢@{ PROP }` agree on the precedences for
+all subexpressions.
+
+For details, consult [the Coq manual](https://coq.inria.fr/refman/user-extensions/syntax-extensions.html#simple-factorization-rules).
+
 ## Naming conventions for variables/arguments/hypotheses
 
 ### small letters
diff --git a/theories/bi/interface.v b/theories/bi/interface.v
index 4eb80f6c79b4ab114300d79bb226b66cf1d93ad9..fd09f4c2f8d34661e64afa9e9eadfdf9df58c82f 100644
--- a/theories/bi/interface.v
+++ b/theories/bi/interface.v
@@ -260,14 +260,14 @@ Instance bi_rewrite_relation (PROP : bi) : RewriteRelation (@bi_entails PROP) :=
 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 "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.
+Notation "P '⊣⊢@{' PROP } Q" := (equiv (A:=bi_car PROP) P%I Q%I) (only parsing) : stdpp_scope.
 Notation "(⊣⊢)" := (equiv (A:=bi_car _)) (only parsing) : stdpp_scope.
-Notation "(⊣⊢@{ PROP } )" := (equiv (A:=bi_car PROP)) (only parsing) : stdpp_scope.
+Notation "('⊣⊢@{' PROP } )" := (equiv (A:=bi_car PROP)) (only parsing) : stdpp_scope.
 
 Notation "P -∗ Q" := (P ⊢ Q) : stdpp_scope.
 
diff --git a/theories/bi/notation.v b/theories/bi/notation.v
index 9534481981ed54127029c7da3b46d06d01bdb884..8b268c974c55fb88b72ca229379861f7b577a495 100644
--- a/theories/bi/notation.v
+++ b/theories/bi/notation.v
@@ -3,10 +3,13 @@
 (** Turnstiles *)
 Reserved Notation "P ⊢ Q" (at level 99, Q at level 200, right associativity).
 Reserved Notation "P '⊢@{' PROP } Q" (at level 99, Q at level 200, right associativity).
-Reserved Notation "('⊢@{' PROP } )" (at level 99).
+Reserved Notation "(⊢)".
+Reserved Notation "('⊢@{' PROP } )".
+
 Reserved Notation "P ⊣⊢ Q" (at level 95, no associativity).
 Reserved Notation "P '⊣⊢@{' PROP } Q" (at level 95, no associativity).
-Reserved Notation "('⊣⊢@{' PROP } )" (at level 95).
+Reserved Notation "(⊣⊢)".
+Reserved Notation "('⊣⊢@{' PROP } )".
 
 (** BI connectives *)
 Reserved Notation "'emp'".