fix or silence 8.20 warnings

_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

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,