diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 8addea4b7c2492262d47e66b1dffa9a52c6d603b..cf8dbe12e29cdf72ea5c1487faceea1514622de2 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -45,10 +45,10 @@ variables:
 ## Build jobs
 
 # The newest version runs with timing.
-build-coq.8.19.1:
+build-coq.8.20.0:
   <<: *template
   variables:
-    OPAM_PINS: "coq version 8.19.1"
+    OPAM_PINS: "coq version 8.20.0"
     DENY_WARNINGS: "1"
     MANGLE_NAMES: "1"
     OPAM_PKG: "1"
@@ -59,22 +59,28 @@ build-coq.8.19.1:
   interruptible: false
 
 # The newest version also runs in MRs, without timing.
-build-coq.8.19.1-mr:
+build-coq.8.20.0-mr:
   <<: *template
   <<: *only_mr
   variables:
-    OPAM_PINS: "coq version 8.19.1"
+    OPAM_PINS: "coq version 8.20.0"
     DENY_WARNINGS: "1"
     MANGLE_NAMES: "1"
 
 # Also ensure Dune works.
-build-coq.8.19.1-dune:
+build-coq.8.20.0-dune:
   <<: *template
   <<: *branches_and_mr
   variables:
-    OPAM_PINS: "coq version 8.19.1   dune version 3.15.2"
+    OPAM_PINS: "coq version 8.20.0   dune version 3.15.2"
     MAKE_TARGET: "dune"
 
+build-coq.8.19.1:
+  <<: *template
+  variables:
+    OPAM_PINS: "coq version 8.19.1"
+    DENY_WARNINGS: "1"
+
 # The oldest version runs in MRs, without name mangling.
 build-coq.8.18.0:
   <<: *template
diff --git a/Makefile.coq.local b/Makefile.coq.local
index 4df3f5c55041e5c07ff5fd0f59b0cef7fdac899b..4babb6f2392b41028fd768806a55592f1549c34a 100644
--- a/Makefile.coq.local
+++ b/Makefile.coq.local
@@ -4,6 +4,11 @@ NO_TEST:=
 # use MAKE_REF=1 to generate new reference files
 MAKE_REF:=
 
+# Only test reference output on known versions of Coq, to avoid blocking
+# Coq CI when they change the printing a little.
+# Need to make this a lazy variable (`=` instead of `:=`) since COQ_VERSION is only set later.
+COQ_REF=$(shell echo "$(COQ_VERSION)" | grep -E "^8\.(20)\." -q && echo 1)
+
 # Run tests interleaved with main build.  They have to be in the same target for this.
 real-all: style $(if $(NO_TEST),,test)
 
@@ -26,10 +31,6 @@ test: $(TESTFILES:.v=.vo)
 .PHONY: test
 
 COQ_TEST=$(COQTOP) $(COQDEBUG) -batch -test-mode
-# These versions of Coq are known to have different output so we don't test them.
-# Need to make this a lazy variable (`=` instead of `:=`) since COQ_VERSION is only set later.
-# Make sure to recognize both 8.$NUM.0 and 8.$NUM+alpha.
-COQ_NOREF=$(shell echo "$(COQ_VERSION)" | grep -E "^8\.(16|17|18|20|21)[.+]" -q && echo 1)
 
 tests/.coqdeps.d: $(TESTFILES)
 	$(SHOW)'COQDEP TESTFILES'
@@ -46,14 +47,15 @@ tests/.coqdeps.d: $(TESTFILES)
 # - Cleanup, and mark as done for make.
 $(TESTFILES:.v=.vo): %.vo: %.v $(if $(MAKE_REF),,%.ref) $(NORMALIZER)
 	$(HIDE)REF=$*".ref" && \
-	  echo "COQTEST$(if $(COQ_NOREF), [ref diff ignored],$(if $(MAKE_REF), [make ref],)) $< (ref: $$REF)" && \
+	  echo "COQTEST$(if $(COQ_REF),$(if $(MAKE_REF), [make ref],), [ref diff ignored]) $< (ref: $$REF)" && \
 	  TMPFILE="$$(mktemp)" && \
 	  unset OCAMLRUNPARAM && \
 	  $(TIMER) $(COQ_TEST) $(COQFLAGS) $(COQLIBS) -load-vernac-source $< > "$$TMPFILE" && \
 	  sed -E -f $(NORMALIZER) "$$TMPFILE" > "$$TMPFILE".new && \
 	  mv "$$TMPFILE".new "$$TMPFILE" && \
-	  $(if $(COQ_NOREF), (diff --strip-trailing-cr -u "$$REF" "$$TMPFILE" || true) , \
-	    $(if $(MAKE_REF),mv "$$TMPFILE" "$$REF",diff --strip-trailing-cr -u "$$REF" "$$TMPFILE") \
+	  $(if $(COQ_REF),\
+	    $(if $(MAKE_REF),mv "$$TMPFILE" "$$REF",diff --strip-trailing-cr -u "$$REF" "$$TMPFILE"), \
+	    (diff --strip-trailing-cr -u "$$REF" "$$TMPFILE" || true) \
 	  ) && \
 	  rm -f "$$TMPFILE" && \
 	  touch $@
diff --git a/README.md b/README.md
index c246c328fc62570bc911fed1044fafc1f40a410b..4d3f85b15d1a640635b310a4bc6be1e0fb0419ec 100644
--- a/README.md
+++ b/README.md
@@ -30,7 +30,7 @@ Importing Iris has some side effects as the library sets some global options.
 
 This version is known to compile with:
 
- - Coq 8.18.0 / 8.19.1
+ - Coq 8.18.0 / 8.19.1 / 8.20.0
  - A development version of [std++](https://gitlab.mpi-sws.org/iris/stdpp)
 
 Generally we always aim to support the last two stable Coq releases. Support for
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/coq-iris.opam b/coq-iris.opam
index 3d74529e801e506424ac4e70716a286abd3fd890..49010f8ef48f1971df654a306573d2481fc42565 100644
--- a/coq-iris.opam
+++ b/coq-iris.opam
@@ -27,7 +27,7 @@ tags: [
 ]
 
 depends: [
-  "coq" { (>= "8.18" & < "8.20~") | (= "dev") }
+  "coq" { (>= "8.18" & < "8.21~") | (= "dev") }
   "coq-stdpp" { (= "dev.2024-09-11.0.f6973baf") | (= "dev") }
 ]
 
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,
diff --git a/tests/bi.ref b/tests/bi.ref
index faa15d658329457d2cb0aa426ea563bc2dff575f..9aed176aa683bb6138146eb94dcb546734d9b767 100644
--- a/tests/bi.ref
+++ b/tests/bi.ref
@@ -5,21 +5,17 @@ m : gmap nat nat
 The term "m" has type "gmap nat nat" while it is expected to have type
  "gmap nat Z" (cannot unify "nat" and "Z").
 The command has indeed failed with message:
-Unable to satisfy the following constraints:
 In environment:
 PROP : bi
 P : PROP
-
-?p : "Persistent (|==> P)"
-
+Could not find an instance for the following existential variables:
+?p : Persistent (|==> P)
 The command has indeed failed with message:
-Unable to satisfy the following constraints:
 In environment:
 PROP : bi
 P : PROP
-
-?p : "Persistent (â–  P)"
-
+Could not find an instance for the following existential variables:
+?p : Persistent (â–  P)
 "match_def_unfold_fail"
      : string
 The command has indeed failed with message:
diff --git a/tests/heap_lang.ref b/tests/heap_lang.ref
index 613d78114412de1c14359c7d228eb37c33171eed..8af930a4f747d39fcbf2c87f535b525c921affdc 100644
--- a/tests/heap_lang.ref
+++ b/tests/heap_lang.ref
@@ -232,10 +232,10 @@ Tactic failure: wp_pure: "Hcred" is not fresh.
   q3 : Qp
   v4 : val
   q4 : Qp
-  H : ((✓ (DfracOwn q3 ⋅ DfracOwn q4) ∧ v3 = v4)
-       ∧ ✓ (DfracOwn q2 ⋅ (DfracOwn q3 ⋅ DfracOwn q4)) ∧ v2 = v3)
-      ∧ ✓ (DfracOwn q1 ⋅ (DfracOwn q2 ⋅ (DfracOwn q3 ⋅ DfracOwn q4)))
-        ∧ v1 = v2
+  H :
+    ((✓ (DfracOwn q3 ⋅ DfracOwn q4) ∧ v3 = v4)
+     ∧ ✓ (DfracOwn q2 ⋅ (DfracOwn q3 ⋅ DfracOwn q4)) ∧ v2 = v3)
+    ∧ ✓ (DfracOwn q1 ⋅ (DfracOwn q2 ⋅ (DfracOwn q3 ⋅ DfracOwn q4))) ∧ v1 = v2
   ============================
   --------------------------------------∗
   ⌜(q1 + (q2 + (q3 + q4)) ≤ 1)%Qp⌝ ∗ ⌜v1 = v2⌝ ∗ ⌜
diff --git a/tests/proofmode.ref b/tests/proofmode.ref
index 58da080bdfedd4f0d1fc38a5407f1ee5144fdaaf..402665b1e9d7d22cd906e29f3e7b9870045912be 100644
--- a/tests/proofmode.ref
+++ b/tests/proofmode.ref
@@ -708,8 +708,8 @@ No applicable tactic.
   
   PROP : bi
   Ψ, Φ : nat → PROP
-  HP : ∀ (f : nat → nat) (y : nat),
-         TCEq f (λ x : nat, x + 10) → Ψ (f 1) -∗ Φ y
+  HP :
+    ∀ (f : nat → nat) (y : nat), TCEq f (λ x : nat, x + 10) → Ψ (f 1) -∗ Φ y
   ============================
   "H" : Ψ 11
   --------------------------------------∗