switch reftesting to Coq 8.20

Makefile.coq.local

@@ -24,10 +24,10 @@ 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.
+# 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.
-# 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)
+COQ_REF=$(shell echo "$(COQ_VERSION)" | grep -E "^8\.(20)\." -q && echo 1)
 
 tests/.coqdeps.d: $(TESTFILES)
 	$(SHOW)'COQDEP TESTFILES'
@@ -44,14 +44,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/bitvector_tactics.ref

@@ -21,11 +21,12 @@
   data : list (bv 64)
   H : bv_unsigned l < bv_unsigned r
   H0 : bv_unsigned r ≤ Z.of_nat (length data)
-  H1 : ¬ bv_swrap 128 (bv_unsigned l) >=
-         bv_swrap 128
-           (bv_wrap 64
-              (bv_wrap 64 (bv_unsigned r - bv_unsigned l) `div` 2 ^ 1 +
-               bv_unsigned l + 0))
+  H1 :
+    ¬ bv_swrap 128 (bv_unsigned l) >=
+      bv_swrap 128
+        (bv_wrap 64
+           (bv_wrap 64 (bv_unsigned r - bv_unsigned l) `div` 2 ^ 1 +
+            bv_unsigned l + 0))
   ============================
   bv_unsigned l <
   bv_wrap 64
@@ -46,9 +47,10 @@ goal 2 is:
   
   i, n : bv 64
   H : bv_unsigned i < bv_unsigned n
-  H0 : bv_wrap 64
-         (bv_unsigned n + bv_wrap 64 (- bv_wrap 64 (bv_unsigned i + 1) - 1) +
-          1) ≠ 0%Z
+  H0 :
+    bv_wrap 64
+      (bv_unsigned n + bv_wrap 64 (- bv_wrap 64 (bv_unsigned i + 1) - 1) + 1)
+    ≠ 0%Z
   ============================
   bv_wrap 64 (bv_unsigned i + 1) < bv_unsigned n
 1 goal