diff --git a/tests/proofmode.v b/tests/proofmode.v
index 9ff9c88a3a6b7644c89d1791ad3881d7ef934149..a68c061d10fb5cc4ccf3bcc7a9d0e8bb9b789e8d 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -5,10 +5,6 @@ Section tests.
 Context {PROP : sbi}.
 Implicit Types P Q R : PROP.
 
-Lemma test_sbi_internal_eq_annot_sections P :
-  ⊢@{PROP} P ≡@{PROP} P ∧ (≡@{PROP}) P P ∧ (P ≡.) P ∧ (.≡ P) P.
-Proof. by iSplit. Qed.
-
 Lemma test_eauto_emp_isplit_biwand P : emp ⊢ P ∗-∗ P.
 Proof. eauto 6. Qed.
 
@@ -825,7 +821,54 @@ Proof.
 Qed.
 End tests.
 
-(** Test specifically if certain things print correctly. *)
+Section parsing_tests.
+Context {PROP : sbi}.
+Implicit Types P : PROP.
+
+(** Test notations for (bi)entailment and internal equality. These tests are
+especially extensive because of past problems such as
+https://gitlab.mpi-sws.org/iris/iris/-/issues/302. *)
+Lemma test_bi_emp_valid : ⊢@{PROP} True.
+Proof. naive_solver. Qed.
+
+Lemma test_bi_emp_valid_parens : (⊢@{PROP} True) ∧ ((⊢@{PROP} True)).
+Proof. naive_solver. Qed.
+
+Lemma test_bi_emp_valid_parens_space_open : ( ⊢@{PROP} True).
+Proof. naive_solver. Qed.
+
+Lemma test_bi_emp_valid_parens_space_close : (⊢@{PROP} True ).
+Proof. naive_solver. Qed.
+
+Lemma test_entails_annot_sections P :
+  (P ⊢@{PROP} P) ∧ (⊢@{PROP}) P P ∧ (P ⊢.) P ∧ (.⊢ P) P ∧
+  (P ⊣⊢@{PROP} P) ∧ (⊣⊢@{PROP}) P P ∧ (P ⊣⊢.) P ∧ (.⊣⊢ P) P.
+Proof. naive_solver. Qed.
+
+Lemma test_entails_annot_sections_parens P :
+  ((P ⊢@{PROP} P)) ∧ ((⊢@{PROP})) P P ∧ ((P ⊢.)) P ∧ ((.⊢ P)) P ∧
+  ((P ⊣⊢@{PROP} P)) ∧ ((⊣⊢@{PROP})) P P ∧ ((P ⊣⊢.)) P ∧ ((.⊣⊢ P)) P.
+Proof. naive_solver. Qed.
+
+Lemma test_entails_annot_sections_space_open P :
+  ( P ⊢@{PROP} P) ∧ ( P ⊢.) P ∧
+  ( P ⊣⊢@{PROP} P) ∧ ( P ⊣⊢.) P.
+Proof. naive_solver. Qed.
+
+Lemma test_entails_annot_sections_space_close P :
+  (P ⊢@{PROP} P ) ∧ (⊢@{PROP} ) P P ∧ (.⊢ P ) P ∧
+  (P ⊣⊢@{PROP} P ) ∧ (⊣⊢@{PROP} ) P P ∧ (.⊣⊢ P ) P.
+Proof. naive_solver. Qed.
+
+Lemma test_sbi_internal_eq_annot_sections P :
+  ⊢@{PROP}
+    P ≡@{PROP} P ∧ (≡@{PROP}) P P ∧ (P ≡.) P ∧ (.≡ P) P ∧
+    ((P ≡@{PROP} P)) ∧ ((≡@{PROP})) P P ∧ ((P ≡.)) P ∧ ((.≡ P)) P ∧
+    ( P ≡@{PROP} P) ∧ ( P ≡.) P ∧
+    (P ≡@{PROP} P ) ∧ (≡@{PROP} ) P P ∧ (.≡ P ) P.
+Proof. naive_solver. Qed.
+End parsing_tests.
+
 Section printing_tests.
 Context {PROP : sbi} `{!BiFUpd PROP}.
 Implicit Types P Q R : PROP.
diff --git a/tests/proofmode_ascii.v b/tests/proofmode_ascii.v
index f279d738203bbb8f66ba10488d1fa35259e5b3d4..4c55aeb66f3c936c64319945f2e38dad225e807c 100644
--- a/tests/proofmode_ascii.v
+++ b/tests/proofmode_ascii.v
@@ -258,3 +258,41 @@ Section monpred_tests.
   Qed.
 
 End monpred_tests.
+
+(** Test specifically if certain things parse correctly. *)
+Section parsing_tests.
+Context {PROP : sbi}.
+Implicit Types P : PROP.
+
+Lemma test_bi_emp_valid : |--@{PROP} True.
+Proof. naive_solver. Qed.
+
+Lemma test_bi_emp_valid_parens : (|--@{PROP} True) /\ ((|--@{PROP} True)).
+Proof. naive_solver. Qed.
+
+Lemma test_bi_emp_valid_parens_space_open : ( |--@{PROP} True).
+Proof. naive_solver. Qed.
+
+Lemma test_bi_emp_valid_parens_space_close : (|--@{PROP} True ).
+Proof. naive_solver. Qed.
+
+Lemma test_entails_annot_sections P :
+  (P |--@{PROP} P) /\ (|--@{PROP}) P P /\
+  (P -|-@{PROP} P) /\ (-|-@{PROP}) P P.
+Proof. naive_solver. Qed.
+
+Lemma test_entails_annot_sections_parens P :
+  ((P |--@{PROP} P)) /\ ((|--@{PROP})) P P /\
+  ((P -|-@{PROP} P)) /\ ((-|-@{PROP})) P P.
+Proof. naive_solver. Qed.
+
+Lemma test_entails_annot_sections_space_open P :
+  ( P |--@{PROP} P) /\
+  ( P -|-@{PROP} P).
+Proof. naive_solver. Qed.
+
+Lemma test_entails_annot_sections_space_close P :
+  (P |--@{PROP} P ) /\ (|--@{PROP} ) P P /\
+  (P -|-@{PROP} P ) /\ (-|-@{PROP} ) P P.
+Proof. naive_solver. Qed.
+End parsing_tests.
diff --git a/theories/bi/ascii.v b/theories/bi/ascii.v
index 77781344ad1ca0fc96d990e6dc25792791ad95f7..18a7889494fc1c26814b0952f3af0e9a7f99385e 100644
--- a/theories/bi/ascii.v
+++ b/theories/bi/ascii.v
@@ -8,17 +8,17 @@ Notation "P |-- Q" := (P ⊢ Q)
   (at level 99, Q at level 200, right associativity, only parsing) : stdpp_scope.
 Notation "P '|--@{' PROP } Q" := (P ⊢@{PROP} Q) (at level 99, Q at level 200, right associativity, only parsing) : stdpp_scope.
 Notation "(|--)" := (⊢) (only parsing) : stdpp_scope.
-(* FIXME: fix notation *)
-Notation "('|--@{' PROP } )" := (bi_entails (PROP:=PROP)) (only parsing) : stdpp_scope.
+Notation "'(|--@{' PROP } )" := (⊢@{PROP}) (only parsing) : stdpp_scope.
 
 Notation "|-- Q" := (⊢ Q%I) (at level 20, Q at level 200, only parsing) : stdpp_scope.
 Notation "'|--@{' PROP } Q" := (⊢@{PROP} Q) (at level 20, Q at level 200, only parsing) : stdpp_scope.
+(** Work around parsing issues: see [notation.v] for details. *)
+Notation "'(|--@{' PROP } Q )" := (⊢@{PROP} Q) (only parsing) : stdpp_scope.
 
 Notation "P -|- Q" := (P ⊣⊢ Q) (at level 95, no associativity, only parsing) : stdpp_scope.
 Notation "P '-|-@{' PROP } Q" := (P ⊣⊢@{PROP} Q) (at level 95, no associativity, only parsing) : stdpp_scope.
 Notation "(-|-)" := (⊣⊢) (only parsing) : stdpp_scope.
-(* FIXME: fix notation *)
-Notation "('-|-@{' PROP } )" := (equiv (A:=bi_car PROP)) (only parsing) : stdpp_scope.
+Notation "'(-|-@{' PROP } )" := (⊣⊢@{PROP}) (only parsing) : stdpp_scope.
 
 Notation "P -* Q" := (P ⊢ Q)%stdpp (at level 99, Q at level 200, right associativity, only parsing) : stdpp_scope.
 
diff --git a/theories/bi/interface.v b/theories/bi/interface.v
index 3ff2090b44aae3807e1622f409597282a346fe26..845e3a33f02ebedf8d2611765609d5346c28a2ff 100644
--- a/theories/bi/interface.v
+++ b/theories/bi/interface.v
@@ -262,12 +262,14 @@ 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 "(⊢)" := 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 "(⊣⊢)" := (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 ⊣⊢.)" := (equiv (A:=bi_car _) P) (only parsing) : stdpp_scope.
+Notation "(.⊣⊢ Q )" := (λ P, P ≡@{bi_car _} Q) (only parsing) : stdpp_scope.
 
 Notation "P -∗ Q" := (P ⊢ Q) : stdpp_scope.
 
@@ -305,6 +307,10 @@ Typeclasses Opaque bi_emp_valid.
 
 Notation "⊢ Q" := (bi_emp_valid Q%I) : stdpp_scope.
 Notation "'⊢@{' PROP } Q" := (bi_emp_valid (PROP:=PROP) Q%I) (only parsing) : stdpp_scope.
+(** Work around parsing issues: see [notation.v] for details. *)
+Notation "'(⊢@{' PROP } Q )" := (bi_emp_valid (PROP:=PROP) Q%I) (only parsing) : stdpp_scope.
+Notation "(.⊢ Q )" := (λ P, P ⊢ Q) (only parsing) : stdpp_scope.
+Notation "( P ⊢.)" := (bi_entails P) (only parsing) : stdpp_scope.
 
 Module bi.
 Section bi_laws.
diff --git a/theories/bi/notation.v b/theories/bi/notation.v
index 0a8a75a69091a5cb0a3c0fd7cb14b9e2f12e01d3..e6f02661858f300a1edc2b255cc0d8dcf716d985 100644
--- a/theories/bi/notation.v
+++ b/theories/bi/notation.v
@@ -4,15 +4,31 @@
 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 "(⊢)".
-Reserved Notation "('⊢@{' PROP } )".
+Reserved Notation "'(⊢@{' PROP } )".
+Reserved Notation "( P ⊣⊢.)".
+Reserved Notation "(.⊣⊢ Q )".
 
 Reserved Notation "P ⊣⊢ Q" (at level 95, no associativity).
 Reserved Notation "P '⊣⊢@{' PROP } Q" (at level 95, no associativity).
 Reserved Notation "(⊣⊢)".
-Reserved Notation "('⊣⊢@{' PROP } )".
+Reserved Notation "'(⊣⊢@{' PROP } )".
+Reserved Notation "(.⊢ Q )".
+Reserved Notation "( P ⊢.)".
 
 Reserved Notation "⊢ Q" (at level 20, Q at level 200).
 Reserved Notation "'⊢@{' PROP } Q" (at level 20, Q at level 200).
+(** The definition must coincide with "'⊢@{' PROP } Q". *)
+Reserved Notation "'(⊢@{' PROP } Q )".
+(**
+Rationale:
+Notation [( '⊢@{' PROP } )] prevents parsing [(⊢@{PROP} Q)] using the
+[⊢@{PROP} Q] notation; since the latter parse arises from composing two
+notations, it is missed by the automatic left-factorization.
+
+To fix that, we force left-factorization by explicitly composing parentheses with
+['⊢@{' PROP } Q] into the new notation [( '⊢@{' PROP } Q )],
+which successfully undergoes automatic left-factoring. *)
+
 
 (** * BI connectives *)
 Reserved Notation "'emp'".