use Coq 8.20 for reftesting

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 $@

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:

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⌝ ∗ ⌜

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
   --------------------------------------∗