diff --git a/_CoqProject b/_CoqProject
index 7feaf80a32fede7e5d0986cf074b78df44f5da76..78107d894c1259c79f5cb919085e29eaa72bb2e4 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -21,6 +21,8 @@
 -arg -w -arg -unknown-warning
 # Fixing this one requires Coq 8.19
 -arg -w -arg -argument-scope-delimiter
+# https://gitlab.mpi-sws.org/iris/stdpp/-/issues/216
+-arg -w -arg -notation-incompatible-prefix
 
 iris/prelude/options.v
 iris/prelude/prelude.v
diff --git a/iris/bi/notation.v b/iris/bi/notation.v
index d7f4110270a4ebc3e98097fe875d7ae64b0ea335..ce7f4d27160503947ade117afa4d15be1a7b3779 100644
--- a/iris/bi/notation.v
+++ b/iris/bi/notation.v
@@ -33,7 +33,7 @@ which successfully undergoes automatic left-factoring. *)
 
 (** * BI connectives *)
 Reserved Notation "'emp'".
-Reserved Notation "'⌜' φ '⌝'" (at level 1, φ at level 200, format "⌜ φ ⌝").
+Reserved Notation "'⌜' φ '⌝'" (at level 0, φ at level 200, format "⌜ φ ⌝").
 Reserved Notation "P ∗ Q" (at level 80, right associativity, format "P  ∗  '/' Q").
 Reserved Notation "P -∗ Q"
   (at level 99, Q at level 200, right associativity,