From b40126dfc245c07eed112ee251f9757f8b562081 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 11 Sep 2024 18:50:39 +0200
Subject: [PATCH] fix or silence 8.20 warnings

---
 _CoqProject        | 2 ++
 iris/bi/notation.v | 2 +-
 2 files changed, 3 insertions(+), 1 deletion(-)

diff --git a/_CoqProject b/_CoqProject
index 7feaf80a3..78107d894 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 d7f411027..ce7f4d271 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,
-- 
GitLab