Merge branch 'ralf/coq' into 'master'

switch printing tests to 8.19

See merge request iris/iris!1028

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'

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

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

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

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

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:

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