diff --git a/Makefile.coq.local b/Makefile.coq.local
index 53770f4c296e383ad1922dab19da32106257d496..08385834f92455bdfa30f59a2bfde9f19c3f9a20 100644
--- a/Makefile.coq.local
+++ b/Makefile.coq.local
@@ -8,6 +8,7 @@ test: $(TESTFILES:.v=.vo)
.PHONY: test
COQ_TEST=$(COQTOP) $(COQDEBUG) -batch -test-mode
+COQ_OLD=$(shell echo "$(COQ_VERSION)" | egrep "^8\.7\b" > /dev/null && echo 1)
COQ_MINOR_VERSION=$(shell echo "$(COQ_VERSION)" | egrep '^[0-9]+\.[0-9]+' -o)
# Can't use pipes because that discards error codes and dash provides no way to control that.
@@ -27,13 +28,13 @@ $(TESTFILES:.v=.vo): %.vo: %.v $(if $(MAKE_REF),,%.ref)
else \
REF="tests/$$TEST.ref"; \
fi && \
- echo $(if $(MAKE_REF),"COQTEST [ref] `basename "$$REF"`","COQTEST `basename "$$REF"`") && \
+ echo $(if $(MAKE_REF),"COQTEST [ref] `basename "$$REF"`","COQTEST$(if $(COQ_OLD), [ignored],) `basename "$$REF"`") && \
TMPFILE="$$(mktemp)" && \
$(TIMER) $(COQ_TEST) $(COQFLAGS) $(COQLIBS) -load-vernac-source $< > "$$TMPFILE" && \
($(REF_FILTER) < "$$TMPFILE" > "$$TMPFILE.filtered" || true) && \
$(if $(MAKE_REF), \
mv "$$TMPFILE.filtered" "$$REF", \
- diff -u "$$REF" "$$TMPFILE.filtered" \
+ $(if $(COQ_OLD),true,diff -u "$$REF" "$$TMPFILE.filtered") \
) && \
rm -f "$$TMPFILE" "$$TMPFILE.filtered" && \
touch $@
diff --git a/tests/atomic.8.7.ref b/tests/atomic.8.7.ref
deleted file mode 100644
index af5aa0bbc9bfb2f551a55650446276679623defe..0000000000000000000000000000000000000000
--- a/tests/atomic.8.7.ref
+++ /dev/null
@@ -1,369 +0,0 @@
-1 subgoal
-
- Σ : gFunctors
- heapG0 : heapG Σ
- P : val → iProp Σ
- ============================
- <<< ∀ x : val, P x >>> code @ ⊤ <<< ∃ y : val, P y, RET #() >>>
-1 subgoal
-
- Σ : gFunctors
- heapG0 : heapG Σ
- P : val → iProp Σ
- Q : iPropI Σ
- Φ : language.val heap_lang → iProp Σ
- ============================
- _ : Q
- "AU" : AU << ∀ x : val, P x >> @ ⊤, ∅ << ∃ y : val, P y, COMM Q -∗ Φ #() >>
- --------------------------------------∗
- WP code {{ v, Φ v }}
-
-1 subgoal
-
- Σ : gFunctors
- heapG0 : heapG Σ
- P : val → iProp Σ
- Q : iPropI Σ
- Φ : language.val heap_lang → iProp Σ
- ============================
- _ : Q
- _ : AACC << ∀ x : val, P x
- ABORT AU << ∀ x : val, P x >> @ ⊤, ∅
- << ∃ y : val, P y, COMM Q -∗ Φ #() >> >> @ ⊤, ∅
- << ∃ y : val, P y, COMM Q -∗ Φ #() >>
- --------------------------------------∗
- WP code {{ v, Φ v }}
-
-1 subgoal
-
- Σ : gFunctors
- heapG0 : heapG Σ
- l : loc
- ============================
- <<< ∀ x : val, l ↦ x >>> code @ ⊤ <<< l ↦ x, RET #() >>>
-1 subgoal
-
- Σ : gFunctors
- heapG0 : heapG Σ
- l : loc
- Q : iPropI Σ
- Φ : language.val heap_lang → iProp Σ
- ============================
- _ : Q
- "AU" : AU << ∀ x : val, l ↦ x >> @ ⊤, ∅ << l ↦ x, COMM Q -∗ Φ #() >>
- --------------------------------------∗
- WP code {{ v, Φ v }}
-
-1 subgoal
-
- Σ : gFunctors
- heapG0 : heapG Σ
- l : loc
- Q : iPropI Σ
- Φ : language.val heap_lang → iProp Σ
- ============================
- _ : Q
- _ : AACC << ∀ x : val, l ↦ x
- ABORT AU << ∀ x : val, l ↦ x >> @ ⊤, ∅
- << l ↦ x, COMM Q -∗ Φ #() >> >> @ ⊤, ∅
- << l ↦ x, COMM Q -∗ Φ #() >>
- --------------------------------------∗
- WP code {{ v, Φ v }}
-
-1 subgoal
-
- Σ : gFunctors
- heapG0 : heapG Σ
- l : loc
- ============================
- <<< l ↦ #() >>> code @ ⊤ <<< ∃ y : val, l ↦ y, RET #() >>>
-1 subgoal
-
- Σ : gFunctors
- heapG0 : heapG Σ
- l : loc
- Q : iPropI Σ
- Φ : language.val heap_lang → iProp Σ
- ============================
- _ : Q
- "AU" : AU << l ↦ #() >> @ ⊤, ∅ << ∃ y : val, l ↦ y, COMM Q -∗ Φ #() >>
- --------------------------------------∗
- WP code {{ v, Φ v }}
-
-1 subgoal
-
- Σ : gFunctors
- heapG0 : heapG Σ
- l : loc
- Q : iPropI Σ
- Φ : language.val heap_lang → iProp Σ
- ============================
- _ : Q
- _ : AACC << l ↦ #()
- ABORT AU << l ↦ #() >> @ ⊤, ∅
- << ∃ y : val, l ↦ y, COMM Q -∗ Φ #() >> >> @ ⊤, ∅
- << ∃ y : val, l ↦ y, COMM Q -∗ Φ #() >>
- --------------------------------------∗
- WP code {{ v, Φ v }}
-
-1 subgoal
-
- Σ : gFunctors
- heapG0 : heapG Σ
- l : loc
- ============================
- <<< l ↦ #() >>> code @ ⊤ <<< l ↦ #(), RET #() >>>
-1 subgoal
-
- Σ : gFunctors
- heapG0 : heapG Σ
- l : loc
- Q : iPropI Σ
- Φ : language.val heap_lang → iProp Σ
- ============================
- _ : Q
- "AU" : AU << l ↦ #() >> @ ⊤, ∅ << l ↦ #(), COMM Q -∗ Φ #() >>
- --------------------------------------∗
- WP code {{ v, Φ v }}
-
-1 subgoal
-
- Σ : gFunctors
- heapG0 : heapG Σ
- l : loc
- Q : iPropI Σ
- Φ : language.val heap_lang → iProp Σ
- ============================
- _ : Q
- _ : AACC << l ↦ #()
- ABORT AU << l ↦ #() >> @ ⊤, ∅ << l ↦ #(), COMM Q -∗ Φ #() >> >>
- @ ⊤, ∅ << l ↦ #(), COMM Q -∗ Φ #() >>
- --------------------------------------∗
- WP code {{ v, Φ v }}
-
-"Now come the long pre/post tests"
- : string
-1 subgoal
-
- Σ : gFunctors
- heapG0 : heapG Σ
- l : loc
- ============================
- <<< ∀ x : val, l ↦ x ∗ l ↦ x >>> code @ ⊤ <<< ∃ y : val, l ↦ y, RET #() >>>
-1 subgoal
-
- Σ : gFunctors
- heapG0 : heapG Σ
- l : loc
- Q : iPropI Σ
- Φ : language.val heap_lang → iProp Σ
- ============================
- _ : Q
- "AU" : AU << ∀ x : val, l ↦ x ∗ l ↦ x >> @ ⊤, ∅
- << ∃ y : val, l ↦ y, COMM Q -∗ Φ #() >>
- --------------------------------------∗
- WP code {{ v, Φ v }}
-
-1 subgoal
-
- Σ : gFunctors
- heapG0 : heapG Σ
- l : loc
- ============================
- <<< ∀ x : val, l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>>
- code @ ⊤
- <<< ∃ y : val, l ↦ y, RET #() >>>
-1 subgoal
-
- Σ : gFunctors
- heapG0 : heapG Σ
- l : loc
- Q : iPropI Σ
- Φ : language.val heap_lang → iProp Σ
- ============================
- _ : Q
- "AU" : AU << ∀ x : val, l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>
- @ ⊤, ∅ << ∃ y : val, l ↦ y, COMM Q -∗ Φ #() >>
- --------------------------------------∗
- WP code {{ v, Φ v }}
-
-1 subgoal
-
- Σ : gFunctors
- heapG0 : heapG Σ
- l : loc
- ============================
- <<< ∀ xx : val, l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>>
- code @ ⊤
- <<< ∃ yyyy : val, l ↦ yyyy ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx,
- RET #() >>>
-1 subgoal
-
- Σ : gFunctors
- heapG0 : heapG Σ
- l : loc
- Q : iPropI Σ
- Φ : language.val heap_lang → iProp Σ
- ============================
- _ : Q
- _ : AU << ∀ xx : val, l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >> @ ⊤, ∅
- << ∃ yyyy : val, l ↦ yyyy
- ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx,
- COMM Q -∗ Φ #() >>
- --------------------------------------∗
- WP code {{ v, Φ v }}
-
-1 subgoal
-
- Σ : gFunctors
- heapG0 : heapG Σ
- l : loc
- ============================
- <<< ∀ x : val, l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>>
- code @ ⊤
- <<< l ↦ x, RET #() >>>
-1 subgoal
-
- Σ : gFunctors
- heapG0 : heapG Σ
- l : loc
- Q : iPropI Σ
- Φ : language.val heap_lang → iProp Σ
- ============================
- _ : Q
- "AU" : AU << ∀ x : val, l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >> @ ⊤, ∅
- << l ↦ x, COMM Q -∗ Φ #() >>
- --------------------------------------∗
- WP code {{ v, Φ v }}
-
-1 subgoal
-
- Σ : gFunctors
- heapG0 : heapG Σ
- l : loc
- x : val
- ============================
- <<< l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>>
- code @ ⊤
- <<< ∃ y : val, l ↦ y, RET #() >>>
-1 subgoal
-
- Σ : gFunctors
- heapG0 : heapG Σ
- l : loc
- x : val
- Q : iPropI Σ
- Φ : language.val heap_lang → iProp Σ
- ============================
- _ : Q
- "AU" : AU << l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >> @ ⊤, ∅
- << ∃ y : val, l ↦ y, COMM Q -∗ Φ #() >>
- --------------------------------------∗
- WP code {{ v, Φ v }}
-
-1 subgoal
-
- Σ : gFunctors
- heapG0 : heapG Σ
- l : loc
- x : val
- ============================
- <<< l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>>
- code @ ⊤
- <<< l ↦ #(), RET #() >>>
-1 subgoal
-
- Σ : gFunctors
- heapG0 : heapG Σ
- l : loc
- x : val
- Q : iPropI Σ
- Φ : language.val heap_lang → iProp Σ
- ============================
- _ : Q
- "AU" : AU << l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >> @ ⊤, ∅
- << l ↦ #(), COMM Q -∗ Φ #() >>
- --------------------------------------∗
- WP code {{ v, Φ v }}
-
-1 subgoal
-
- Σ : gFunctors
- heapG0 : heapG Σ
- l : loc
- xx, yyyy : val
- ============================
- <<< l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>>
- code @ ⊤
- <<< l ↦ yyyy, RET #() >>>
-1 subgoal
-
- Σ : gFunctors
- heapG0 : heapG Σ
- l : loc
- xx, yyyy : val
- Q : iPropI Σ
- Φ : language.val heap_lang → iProp Σ
- ============================
- _ : Q
- "AU" : AU << l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>
- @ ⊤, ∅ << l ↦ yyyy, COMM Q -∗ Φ #() >>
- --------------------------------------∗
- WP code {{ v, Φ v }}
-
-1 subgoal
-
- Σ : gFunctors
- heapG0 : heapG Σ
- l : loc
- xx, yyyy : val
- ============================
- <<< l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>>
- code @ ⊤
- <<< l ↦ yyyy ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx,
- RET #() >>>
-1 subgoal
-
- Σ : gFunctors
- heapG0 : heapG Σ
- l : loc
- xx, yyyy : val
- Q : iPropI Σ
- Φ : language.val heap_lang → iProp Σ
- ============================
- _ : Q
- "AU" : AU << l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >> @ ⊤, ∅
- << l ↦ yyyy ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx,
- COMM Q -∗ Φ #() >>
- --------------------------------------∗
- WP code {{ v, Φ v }}
-
-"Prettification"
- : string
-1 subgoal
-
- Σ : gFunctors
- heapG0 : heapG Σ
- P : val → iProp Σ
- ============================
- --------------------------------------∗
- ∀ Φ : language.val heap_lang → iProp Σ,
- AU << ∀ x : val, P x >> @ ⊤, ∅ << ∃ y : val, P y, COMM Φ #() >>
- -∗ WP ! #0 {{ v, Φ v }}
-
-1 subgoal
-
- Σ : gFunctors
- heapG0 : heapG Σ
- P : val → iProp Σ
- Φ : language.val heap_lang → iProp Σ
- ============================
- "AU" : ∃ x : val,
- P x
- ∗ (P x
- ={∅,⊤}=∗ AU << ∀ x0 : val, P x0 >> @ ⊤, ∅
- << ∃ y : val, P y, COMM Φ #() >>)
- ∧ (∀ x0 : val, P x0 ={∅,⊤}=∗ Φ #())
- --------------------------------------∗
- WP ! #0 @ ∅ {{ v, |={∅,⊤}=> Φ v }}
-