diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index dc02a8b03c64815da4410c753909b3018b65c6c5..0c30b9feecb62e45decb05fe7b86f0b4027f2775 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -29,6 +29,7 @@ variables:
 build-coq.dev:
   <<: *template
   variables:
+    BUILD_TARGET: "ref" # don't check test output
     OPAM_PINS: "coq version dev"
     VALIDATE: "1"
 
diff --git a/Makefile b/Makefile
index e089b03f567d9b4b180f27a5fa5ff9c0ae866729..e15b27a375892bda2de8b828dacc81c79e75759e 100644
--- a/Makefile
+++ b/Makefile
@@ -8,7 +8,7 @@ all: Makefile.coq
 
 clean: Makefile.coq
 	+@make -f Makefile.coq clean
-	find theories \( -name "*.v.d" -o -name "*.vo" -o -name "*.aux" -o -name "*.cache" -o -name "*.glob" -o -name "*.vio" \) -print -delete
+	find theories $$(test -d tests && echo tests) \( -name "*.v.d" -o -name "*.vo" -o -name "*.aux" -o -name "*.cache" -o -name "*.glob" -o -name "*.vio" \) -print -delete
 	rm -f Makefile.coq
 .PHONY: clean
 
@@ -33,7 +33,7 @@ build-dep: build-dep/opam phony
 	@# dependencies, but does not actually install anything.
 	@# Reinstalling is needed with opam 1 in case the pin already exists, but the builddep
 	@# package changed.
-	@BUILD_DEP_PACKAGE="$$(egrep "^name:" build-dep/opam | sed 's/^name: *"\(.*\)" */\1/')"; \
+	@BUILD_DEP_PACKAGE="$$(egrep "^name:" build-dep/opam | sed 's/^name: *"\(.*\)" */\1/')" && \
 	  echo "# Pinning build-dep package." && \
 	  opam pin add -k path $(OPAMFLAGS) "$$BUILD_DEP_PACKAGE".dev build-dep && \
 	  ((! opam --version | grep "^1\." > /dev/null) || ( \
diff --git a/Makefile.coq.local b/Makefile.coq.local
new file mode 100644
index 0000000000000000000000000000000000000000..5b0ccce6a965a649e6ab07cc0233b40bb87234dc
--- /dev/null
+++ b/Makefile.coq.local
@@ -0,0 +1,25 @@
+# run tests after real-all
+post-all:: test
+
+# the test suite
+TESTFILES=$(wildcard tests/*.v)
+
+test: $(TESTFILES:.v=.vo)
+.PHONY: test
+
+$(TESTFILES:.v=.vo): %.vo: %.v $(VFILES:.v=.vo)
+	$(SHOW)COQC [test] $<
+	$(HIDE)TEST="$$(basename -s .v $<)" && \
+	  TMPFILE="$$(tempfile -p test- -s "-$$TEST")" && \
+	  $(TIMER) $(COQC) $(COQDEBUG) $(TIMING_ARG) $(COQFLAGS) $(COQLIBS) $< $(TIMING_EXTRA) > "$$TMPFILE" && \
+	  (diff --color=auto -u "tests/$$TEST.ref" "$$TMPFILE" || (rm "tests/$$TEST.vo" "$$TMPFILE" && exit 1)) && \
+	  rm "$$TMPFILE"
+
+# a target, for convenience sake, to create the .ref file with the current output
+ref: $(TESTFILES:.v=.ref)
+.PHONY: ref
+
+tests/%.ref: tests/%.v $(VFILES:.v=.vo)
+	$(SHOW)COQC [ref] $<
+	$(HIDE)TEST="$$(basename -s .v $<)" && \
+	  $(TIMER) $(COQC) $(COQDEBUG) $(TIMING_ARG) $(COQFLAGS) $(COQLIBS) $< $(TIMING_EXTRA) > "tests/$$TEST.ref"
diff --git a/_CoqProject b/_CoqProject
index aa2bb70a727766892573925f427a02973e09aead..ead8fc22c808754f0a78242420794907b37e30db 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -109,12 +109,3 @@ theories/proofmode/frame_instances.v
 theories/proofmode/monpred.v
 theories/proofmode/modalities.v
 theories/proofmode/modality_instances.v
-theories/tests/heap_lang.v
-theories/tests/one_shot.v
-theories/tests/proofmode.v
-theories/tests/proofmode_iris.v
-theories/tests/proofmode_monpred.v
-theories/tests/list_reverse.v
-theories/tests/tree_sum.v
-theories/tests/ipm_paper.v
-theories/tests/algebra.v
diff --git a/ci b/ci
index 99c935d2007358fe4028560e96f9c136e608e696..16c8b6107119db3448b6828d3d2757888f2b2376 160000
--- a/ci
+++ b/ci
@@ -1 +1 @@
-Subproject commit 99c935d2007358fe4028560e96f9c136e608e696
+Subproject commit 16c8b6107119db3448b6828d3d2757888f2b2376
diff --git a/tests/algebra.ref b/tests/algebra.ref
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/theories/tests/algebra.v b/tests/algebra.v
similarity index 100%
rename from theories/tests/algebra.v
rename to tests/algebra.v
diff --git a/tests/heap_lang.ref b/tests/heap_lang.ref
new file mode 100644
index 0000000000000000000000000000000000000000..ee58cebaec346975bf8b8de40b50edd2036fdfbe
--- /dev/null
+++ b/tests/heap_lang.ref
@@ -0,0 +1,20 @@
+1 subgoal
+  
+  Σ : gFunctors
+  H : heapG Σ
+  E : coPset
+  ============================
+  --------------------------------------∗
+  WP let: "x" := ref #1 in "x" <- ! "x" + #1;; ! "x" @ E {{ v, ⌜v = #2⌝ }}
+  
+1 subgoal
+  
+  Σ : gFunctors
+  H : heapG Σ
+  E : coPset
+  l : loc
+  ============================
+  _ : l ↦ #1
+  --------------------------------------∗
+  WP #l <- #1 + #1;; ! #l @ E {{ v, ⌜v = #2⌝ }}
+  
diff --git a/theories/tests/heap_lang.v b/tests/heap_lang.v
similarity index 97%
rename from theories/tests/heap_lang.v
rename to tests/heap_lang.v
index 62b74b5e0a6ce9ae1648016cec06161d8219d96e..2e5f2e239a279f057d822be25e85ccb68cd8aad5 100644
--- a/theories/tests/heap_lang.v
+++ b/tests/heap_lang.v
@@ -25,8 +25,9 @@ Section LiftingTests.
 
   Lemma heap_e_spec E : WP heap_e @ E {{ v, ⌜v = #2⌝ }}%I.
   Proof.
-    iIntros "". rewrite /heap_e.
-    wp_alloc l. wp_let. wp_load. wp_op. wp_store. by wp_load.
+    iIntros "". rewrite /heap_e. Show.
+    wp_alloc l. wp_let. wp_load. Show.
+    wp_op. wp_store. by wp_load.
   Qed.
 
   Definition heap_e2 : expr :=
diff --git a/tests/ipm_paper.ref b/tests/ipm_paper.ref
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/theories/tests/ipm_paper.v b/tests/ipm_paper.v
similarity index 100%
rename from theories/tests/ipm_paper.v
rename to tests/ipm_paper.v
diff --git a/tests/list_reverse.ref b/tests/list_reverse.ref
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/theories/tests/list_reverse.v b/tests/list_reverse.v
similarity index 100%
rename from theories/tests/list_reverse.v
rename to tests/list_reverse.v
diff --git a/tests/one_shot.ref b/tests/one_shot.ref
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/theories/tests/one_shot.v b/tests/one_shot.v
similarity index 100%
rename from theories/tests/one_shot.v
rename to tests/one_shot.v
diff --git a/tests/proofmode.ref b/tests/proofmode.ref
new file mode 100644
index 0000000000000000000000000000000000000000..c535692a0c17919272a573fce5a3f7e9b0fd4d53
--- /dev/null
+++ b/tests/proofmode.ref
@@ -0,0 +1,21 @@
+1 subgoal
+  
+  PROP : sbi
+  P, Q : PROP
+  ============================
+  "H2" : ∀ x : nat, ⌜x = 0⌝ ∨ ⌜x = 1⌝
+  --------------------------------------â–¡
+  "H" : □ (P ∨ Q)
+  --------------------------------------∗
+  Q ∨ P
+  
+1 subgoal
+  
+  PROP : sbi
+  P, Q : PROP
+  ============================
+  "H2" : ∀ x : nat, ⌜x = 0⌝ ∨ ⌜x = 1⌝
+  _ : P
+  --------------------------------------â–¡
+  Q ∨ P
+  
diff --git a/theories/tests/proofmode.v b/tests/proofmode.v
similarity index 99%
rename from theories/tests/proofmode.v
rename to tests/proofmode.v
index 3009e5b539adacba015ea223caa510605343e92d..56d90ffdb86317384ffdd6f920fd51714599b04c 100644
--- a/theories/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -8,9 +8,9 @@ Implicit Types P Q R : PROP.
 
 Lemma demo_0 P Q : □ (P ∨ Q) -∗ (∀ x, ⌜x = 0⌝ ∨ ⌜x = 1⌝) → (Q ∨ P).
 Proof.
-  iIntros "H #H2". iDestruct "H" as "###H".
+  iIntros "H #H2". Show. iDestruct "H" as "###H".
   (* should remove the disjunction "H" *)
-  iDestruct "H" as "[#?|#?]"; last by iLeft.
+  iDestruct "H" as "[#?|#?]"; last by iLeft. Show.
   (* should keep the disjunction "H" because it is instantiated *)
   iDestruct ("H2" $! 10) as "[%|%]". done. done.
 Qed.
diff --git a/tests/proofmode_iris.ref b/tests/proofmode_iris.ref
new file mode 100644
index 0000000000000000000000000000000000000000..2530df5c5f60ed41619a9e525d72c40e75846b2c
--- /dev/null
+++ b/tests/proofmode_iris.ref
@@ -0,0 +1,110 @@
+1 subgoal
+  
+  Σ : gFunctors
+  H : invG Σ
+  H0 : cinvG Σ
+  H1 : na_invG Σ
+  N : namespace
+  P : uPredI (iResUR Σ)
+  ============================
+  "H" : inv N (<pers> P)%I
+  "H2" : â–· <pers> P
+  --------------------------------------â–¡
+  |={⊤ ∖ ↑N}=> ▷ <pers> P ∗ (|={⊤}=> ▷ P)
+  
+1 subgoal
+  
+  Σ : gFunctors
+  H : invG Σ
+  H0 : cinvG Σ
+  H1 : na_invG Σ
+  N : namespace
+  P : uPredI (iResUR Σ)
+  ============================
+  "H" : inv N (<pers> P)%I
+  "H2" : â–· <pers> P
+  --------------------------------------â–¡
+  "Hclose" : ▷ <pers> P ={⊤ ∖ ↑N,⊤}=∗ emp
+  --------------------------------------∗
+  |={⊤ ∖ ↑N,⊤}=> ▷ P
+  
+1 subgoal
+  
+  Σ : gFunctors
+  H : invG Σ
+  H0 : cinvG Σ
+  H1 : na_invG Σ
+  γ : gname
+  p : Qp
+  N : namespace
+  P : uPredI (iResUR Σ)
+  ============================
+  _ : cinv N γ (<pers> P)%I
+  "HP" : â–· <pers> P
+  --------------------------------------â–¡
+  "Hown" : cinv_own γ p
+  --------------------------------------∗
+  |={⊤ ∖ ↑N}=> ▷ <pers> P ∗ (|={⊤}=> cinv_own γ p ∗ ▷ P)
+  
+1 subgoal
+  
+  Σ : gFunctors
+  H : invG Σ
+  H0 : cinvG Σ
+  H1 : na_invG Σ
+  γ : gname
+  p : Qp
+  N : namespace
+  P : uPredI (iResUR Σ)
+  ============================
+  _ : cinv N γ (<pers> P)%I
+  "HP" : â–· <pers> P
+  --------------------------------------â–¡
+  "Hown" : cinv_own γ p
+  "Hclose" : ▷ <pers> P ={⊤ ∖ ↑N,⊤}=∗ emp
+  --------------------------------------∗
+  |={⊤ ∖ ↑N,⊤}=> cinv_own γ p ∗ ▷ P
+  
+1 subgoal
+  
+  Σ : gFunctors
+  H : invG Σ
+  H0 : cinvG Σ
+  H1 : na_invG Σ
+  t : na_inv_pool_name
+  N : namespace
+  E1, E2 : coPset
+  P : uPredI (iResUR Σ)
+  H2 : ↑N ⊆ E2
+  ============================
+  _ : na_inv t N (<pers> P)%I
+  "HP" : â–· <pers> P
+  --------------------------------------â–¡
+  "Hown1" : na_own t E1
+  "Hown2" : na_own t (E2 ∖ ↑N)
+  --------------------------------------∗
+  |={⊤}=> (▷ <pers> P ∗ na_own t (E2 ∖ ↑N))
+          ∗ (na_own t E2 ={⊤}=∗ na_own t E1 ∗ na_own t E2 ∗ ▷ P)
+  
+1 subgoal
+  
+  Σ : gFunctors
+  H : invG Σ
+  H0 : cinvG Σ
+  H1 : na_invG Σ
+  t : na_inv_pool_name
+  N : namespace
+  E1, E2 : coPset
+  P : uPredI (iResUR Σ)
+  H2 : ↑N ⊆ E2
+  ============================
+  _ : na_inv t N (<pers> P)%I
+  "HP" : â–· <pers> P
+  --------------------------------------â–¡
+  "Hown1" : na_own t E1
+  "Hown2" : na_own t (E2 ∖ ↑N)
+  "Hclose" : ▷ <pers> P ∗ na_own t (E2 ∖ ↑N) ={⊤}=∗ 
+  id (na_own t E2)
+  --------------------------------------∗
+  |={⊤}=> na_own t E1 ∗ na_own t E2 ∗ ▷ P
+  
diff --git a/theories/tests/proofmode_iris.v b/tests/proofmode_iris.v
similarity index 96%
rename from theories/tests/proofmode_iris.v
rename to tests/proofmode_iris.v
index df20ac3d192317be8b36e77e77f0ea86a12f27dc..a85d637f40bda35d9a89f1e466d93d68762f48d9 100644
--- a/theories/tests/proofmode_iris.v
+++ b/tests/proofmode_iris.v
@@ -63,14 +63,14 @@ Section iris_tests.
   Lemma test_iInv_0 N P: inv N (<pers> P) ={⊤}=∗ ▷ P.
   Proof.
     iIntros "#H".
-    iInv N as "#H2".
+    iInv N as "#H2". Show.
     iModIntro. iSplit; auto.
   Qed.
 
   Lemma test_iInv_0_with_close N P: inv N (<pers> P) ={⊤}=∗ ▷ P.
   Proof.
     iIntros "#H".
-    iInv N as "#H2" "Hclose".
+    iInv N as "#H2" "Hclose". Show.
     iMod ("Hclose" with "H2").
     iModIntro. by iNext.
   Qed.
@@ -88,7 +88,7 @@ Section iris_tests.
     cinv N γ (<pers> P) ∗ cinv_own γ p ={⊤}=∗ cinv_own γ p ∗ ▷ P.
   Proof.
     iIntros "(#?&?)".
-    iInv N as "(#HP&Hown)".
+    iInv N as "(#HP&Hown)". Show.
     iModIntro. iSplit; auto with iFrame.
   Qed.
 
@@ -96,7 +96,7 @@ Section iris_tests.
     cinv N γ (<pers> P) ∗ cinv_own γ p ={⊤}=∗ cinv_own γ p ∗ ▷ P.
   Proof.
     iIntros "(#?&?)".
-    iInv N as "(#HP&Hown)" "Hclose".
+    iInv N as "(#HP&Hown)" "Hclose". Show.
     iMod ("Hclose" with "HP").
     iModIntro. iFrame. by iNext.
   Qed.
@@ -116,7 +116,7 @@ Section iris_tests.
          ⊢ |={⊤}=> na_own t E1 ∗ na_own t E2  ∗ ▷ P.
   Proof.
     iIntros (?) "(#?&Hown1&Hown2)".
-    iInv N as "(#HP&Hown2)".
+    iInv N as "(#HP&Hown2)". Show.
     iModIntro. iSplitL "Hown2"; auto with iFrame.
   Qed.
 
@@ -126,7 +126,7 @@ Section iris_tests.
          ⊢ |={⊤}=> na_own t E1 ∗ na_own t E2  ∗ ▷ P.
   Proof.
     iIntros (?) "(#?&Hown1&Hown2)".
-    iInv N as "(#HP&Hown2)" "Hclose".
+    iInv N as "(#HP&Hown2)" "Hclose". Show.
     iMod ("Hclose" with "[HP Hown2]").
     { iFrame. done. }
     iModIntro. iFrame. by iNext.
diff --git a/tests/proofmode_monpred.ref b/tests/proofmode_monpred.ref
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/theories/tests/proofmode_monpred.v b/tests/proofmode_monpred.v
similarity index 100%
rename from theories/tests/proofmode_monpred.v
rename to tests/proofmode_monpred.v
diff --git a/tests/tree_sum.ref b/tests/tree_sum.ref
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/theories/tests/tree_sum.v b/tests/tree_sum.v
similarity index 100%
rename from theories/tests/tree_sum.v
rename to tests/tree_sum.v