diff --git a/Makefile b/Makefile
index e089b03f567d9b4b180f27a5fa5ff9c0ae866729..f29d7a1172b7c41c7e1b83ddeffdc7a818da46fb 100644
--- a/Makefile
+++ b/Makefile
@@ -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..1f6edfecc6fdd3876ef999c4595c3dde1903a4c4
--- /dev/null
+++ b/Makefile.coq.local
@@ -0,0 +1,24 @@
+# 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) $< $(TIMING_EXTRA) > "$$TMPFILE" && \
+	  diff --color=auto -u "tests/$$TEST.ref" "$$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) $< $(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/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 bd5c516be1b7e553253a22010a2b312087d5b917..ee39d2b8a752f9afe35d2e5cb4b89d7137bbdc68 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