diff --git a/Makefile.coq.local b/Makefile.coq.local
index 1713bc4fa5659b7b61697a2501c99e3a1f92067d..56ee8f18d801c0d3233f01640160c2c52c686c9a 100644
--- a/Makefile.coq.local
+++ b/Makefile.coq.local
@@ -28,8 +28,8 @@ test: $(TESTFILES:.v=.vo)
 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.19.0 and 8.19+alpha.
-COQ_NOREF=$(shell echo "$(COQ_VERSION)" | grep -E "^8\.(19|20)[.+]" -q && echo 1)
+# Make sure to recognize both 8.$NUM.0 and 8.$NUM+alpha.
+COQ_NOREF=$(shell echo "$(COQ_VERSION)" | grep -E "^8\.(16|17|18)[.+]" -q && echo 1)
 
 tests/.coqdeps.d: $(TESTFILES)
 	$(SHOW)'COQDEP TESTFILES'
diff --git a/tests/atomic.ref b/tests/atomic.ref
index 7a3df20814a70a324e3be8d1eefb3b07636436c8..196bc4ccccc825e4470042ae831dd6c783a8aba6 100644
--- a/tests/atomic.ref
+++ b/tests/atomic.ref
@@ -394,6 +394,6 @@
             AU <{ ∃∃ x0 : val, P x0 }>
                @ ⊤ ∖ ∅, ∅
                <{ ∀∀ y : val, P y, COMM Φ #() }>)
-           ∧ (∀ x0 : val, P x0 ={∅,⊤}=∗ Φ #())
+           ∧ ∀ x0 : val, P x0 ={∅,⊤}=∗ Φ #()
   --------------------------------------∗
   WP ! #0 @ ∅ {{ v, |={∅,⊤}=> Φ v }}
diff --git a/tests/ipm_paper.ref b/tests/ipm_paper.ref
index 7ca6491cc009e4d3eff6faf151881b66edf08859..74baaf87b40ee966cdf716b5cbcb4f264b1dab43 100644
--- a/tests/ipm_paper.ref
+++ b/tests/ipm_paper.ref
@@ -84,4 +84,4 @@
   "Hl" : l ↦ #c
   "Hγ" : own γ (Auth c)
   --------------------------------------∗
-  |={⊤ ∖ ↑N}=> ▷ I γ l ∗ (∃ m : nat, ⌜#c = #m ∧ n ≤ m⌝ ∧ C l m)
+  |={⊤ ∖ ↑N}=> ▷ I γ l ∗ ∃ m : nat, ⌜#c = #m ∧ n ≤ m⌝ ∧ C l m
diff --git a/tests/one_shot.ref b/tests/one_shot.ref
index 7ae888dae419bdaade976aef3754b05fee020242..9178f1384c148434e1a5728cdaa81f5f914d8212 100644
--- a/tests/one_shot.ref
+++ b/tests/one_shot.ref
@@ -14,8 +14,7 @@
   _ : own γ Pending
   --------------------------------------∗
   one_shot_inv γ l ∗
-  (⌜InjLV #() = InjLV #()⌝
-   ∨ (∃ n : Z, ⌜InjLV #() = InjRV #n⌝ ∗ own γ (Shot n)))
+  (⌜InjLV #() = InjLV #()⌝ ∨ ∃ n : Z, ⌜InjLV #() = InjRV #n⌝ ∗ own γ (Shot n))
 1 goal
   
   Σ : gFunctors
diff --git a/tests/one_shot_once.ref b/tests/one_shot_once.ref
index b7c8b2e752683a9761a5c54049bf9b07c6239cbb..f5052cdccc1c2fbf112ce7c0773b07a75674a4bd 100644
--- a/tests/one_shot_once.ref
+++ b/tests/one_shot_once.ref
@@ -14,8 +14,7 @@
   _ : own γ (Pending (1 / 2))
   --------------------------------------∗
   one_shot_inv γ l ∗
-  (⌜InjLV #() = InjLV #()⌝
-   ∨ (∃ n : Z, ⌜InjLV #() = InjRV #n⌝ ∗ own γ (Shot n)))
+  (⌜InjLV #() = InjLV #()⌝ ∨ ∃ n : Z, ⌜InjLV #() = InjRV #n⌝ ∗ own γ (Shot n))
 1 goal
   
   Σ : gFunctors
diff --git a/tests/proofmode.ref b/tests/proofmode.ref
index 44b8662fecb74724a3ceb889b14d07cc9f255de5..9e828a7fe0f6840ed776c72834951d77b9056520 100644
--- a/tests/proofmode.ref
+++ b/tests/proofmode.ref
@@ -313,7 +313,7 @@ Tactic failure: iFrame: cannot frame (Φ 0 1).
   P1, P2, P3 : PROP
   ============================
   --------------------------------------∗
-  ▷ (∃ _ : nat, emp)
+  ▷ ∃ _ : nat, emp
 "test_iFrame_or_2"
      : string
 1 goal
@@ -322,7 +322,7 @@ Tactic failure: iFrame: cannot frame (Φ 0 1).
   P1, P2, P3 : PROP
   ============================
   --------------------------------------∗
-  ▷ (∃ x : nat, emp ∧ ⌜x = 0⌝ ∨ emp)
+  ▷ ∃ x : nat, emp ∧ ⌜x = 0⌝ ∨ emp
 "test_iFrame_or_3"
      : string
 1 goal
@@ -331,7 +331,7 @@ Tactic failure: iFrame: cannot frame (Φ 0 1).
   P1, P2, P3 : PROP
   ============================
   --------------------------------------∗
-  ▷ (∃ x : nat, ⌜x = 0⌝)
+  ▷ ∃ x : nat, ⌜x = 0⌝
 "test_iFrame_or_affine_1"
      : string
 1 goal
@@ -341,7 +341,7 @@ Tactic failure: iFrame: cannot frame (Φ 0 1).
   P1, P2, P3 : PROP
   ============================
   --------------------------------------∗
-  ▷ (∃ _ : nat, True)
+  ▷ ∃ _ : nat, True
 "test_iFrame_or_affine_2"
      : string
 1 goal
@@ -351,7 +351,7 @@ Tactic failure: iFrame: cannot frame (Φ 0 1).
   P1, P2, P3 : PROP
   ============================
   --------------------------------------∗
-  ▷ (∃ _ : nat, True)
+  ▷ ∃ _ : nat, True
 "test_iCombine_nested_no_gives"
      : string
 The command has indeed failed with message:
diff --git a/tests/telescopes.ref b/tests/telescopes.ref
index 5ffac672a96f4d0744032ad992218e7c25167e8b..90d7296ebe39f1d0efd42ab472557dd018ca2752 100644
--- a/tests/telescopes.ref
+++ b/tests/telescopes.ref
@@ -94,7 +94,7 @@
   PROP : bi
   x : nat
   ============================
-  "H" : ▷ (∃ x0 : nat, <affine> ⌜x = x0⌝)
+  "H" : ▷ ∃ x0 : nat, <affine> ⌜x = x0⌝
   --------------------------------------∗
   â–· False
 "test3_test"
@@ -112,6 +112,6 @@
   PROP : bi
   x : nat
   ============================
-  "H" : ◇ (∃ x0 : nat, <affine> ⌜x = x0⌝)
+  "H" : ◇ ∃ x0 : nat, <affine> ⌜x = x0⌝
   --------------------------------------∗
   â–· False