diff --git a/_CoqProject b/_CoqProject
index 22bf662a3abbdc11364ec3a6a0af10487f4eda16..4abb13ff22d995c11852419fac6e13c2feba4631 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -61,6 +61,8 @@ iris/pviewshifts.v
 iris/resources.v
 iris/hoare.v
 iris/parameter.v
+iris/tests.v
 barrier/heap_lang.v
 barrier/parameter.v
 barrier/lifting.v
+barrier/tests.v
diff --git a/barrier/heap_lang.v b/barrier/heap_lang.v
index 8ee263c47afd9b39f198a52282c0fbd67f19b003..9ac5c90945da7fa50064f336a3ac6dd71f4056c1 100644
--- a/barrier/heap_lang.v
+++ b/barrier/heap_lang.v
@@ -405,30 +405,6 @@ Proof.
     try (destruct_conjs; eapply fill_not_value2; eassumption).
 Qed.
 
-(** Tests, making sure that stuff works. *)
-Module Tests.
-  Definition add := Op2 plus (Lit 21) (Lit 21).
-
-  Goal forall σ, prim_step add σ (Lit 42) σ None.
-  Proof.
-    apply Op2S.
-  Qed.
-
-  Definition rec := Rec (App (Var 1) (Var 0)). (* fix f x => f x *)
-  Definition rec_app := App rec (Lit 0).
-  Goal forall σ, prim_step rec_app σ rec_app σ None.
-  Proof.
-    move=>?. eapply BetaS. (* Honestly, I have no idea why this works. *)
-    reflexivity.
-  Qed.
-
-  Definition lam := Lam (Op2 plus (Var 0) (Lit 21)).
-  Goal forall σ, prim_step (App lam (Lit 21)) σ add σ None.
-  Proof.
-    move=>?. eapply BetaS. reflexivity.
-  Qed.
-End Tests.
-
 (** Instantiate the Iris language interface. This closes reduction under
     evaluation contexts.
     We could potentially make this a generic construction. *)
diff --git a/barrier/lifting.v b/barrier/lifting.v
index 3aa6c54406b5e916f2e0292612cfcca39dec52e9..7aa8401cb1758f02a252fd770780def698556aa6 100644
--- a/barrier/lifting.v
+++ b/barrier/lifting.v
@@ -1,5 +1,5 @@
+Require Import prelude.gmap iris.lifting.
 Require Export barrier.parameter.
-Require Import prelude.gmap iris.lifting barrier.heap_lang.
 Import uPred.
 
 (* TODO RJ: Figure out a way to to always use our Σ. *)
diff --git a/barrier/parameter.v b/barrier/parameter.v
index 0267acc2c317a41ac8e07a9c801eccf11a3cc0c3..c3d21e55241b3108804e13ade1ef59a5bc1d7e1e 100644
--- a/barrier/parameter.v
+++ b/barrier/parameter.v
@@ -2,4 +2,3 @@ Require Export barrier.heap_lang.
 Require Import iris.parameter.
 
 Definition Σ := IParamConst heap_lang unitRA.
-Print Assumptions Σ.
diff --git a/barrier/tests.v b/barrier/tests.v
new file mode 100644
index 0000000000000000000000000000000000000000..630690101708f3355cca256a91e291aa603f2dfa
--- /dev/null
+++ b/barrier/tests.v
@@ -0,0 +1,30 @@
+(** This file is essentially a bunch of testcases. *)
+Require Import modures.base.
+Require Import barrier.lifting.
+
+Module LangTests.
+  Definition add := Op2 plus (Lit 21) (Lit 21).
+
+  Goal ∀ σ, prim_step add σ (Lit 42) σ None.
+  Proof.
+    apply Op2S.
+  Qed.
+
+  Definition rec := Rec (App (Var 1) (Var 0)). (* fix f x => f x *)
+  Definition rec_app := App rec (Lit 0).
+  Goal ∀ σ, prim_step rec_app σ rec_app σ None.
+  Proof.
+    move=>?. eapply BetaS. (* Honestly, I have no idea why this works. *)
+    reflexivity.
+  Qed.
+
+  Definition lam := Lam (Op2 plus (Var 0) (Lit 21)).
+  Goal ∀ σ, prim_step (App lam (Lit 21)) σ add σ None.
+  Proof.
+    move=>?. eapply BetaS. reflexivity.
+  Qed.
+End LangTests.
+
+Module ParamTests.
+  Print Assumptions Σ.
+End ParamTests.
diff --git a/iris/model.v b/iris/model.v
index 61b2f1566a4e73bd0e7bead9e68a045f1fc45004..f6d146a2b03325f97ad927af83e67d331169c1b5 100644
--- a/iris/model.v
+++ b/iris/model.v
@@ -40,7 +40,3 @@ Instance iProp_fold_inj n Σ : Injective (dist n) (dist n) (@iProp_fold Σ).
 Proof. by intros X Y H; rewrite -(iProp_unfold_fold X) H iProp_unfold_fold. Qed.
 Instance iProp_unfold_inj n Σ : Injective (dist n) (dist n) (@iProp_unfold Σ).
 Proof. by intros X Y H; rewrite -(iProp_fold_unfold X) H iProp_fold_unfold. Qed.
-
-Module Test. (* Make sure we got the notations right. *)
-  Definition iResTest (Σ : iParam) (w : iWld Σ) (p : iPst Σ) (g : iGst Σ) : iRes Σ := Res w p g.
-End Test.
diff --git a/iris/tests.v b/iris/tests.v
new file mode 100644
index 0000000000000000000000000000000000000000..77b46203ca40e7aec1a09b1574417c93c70b759f
--- /dev/null
+++ b/iris/tests.v
@@ -0,0 +1,6 @@
+(** This file tests a bunch of things. *)
+Require Import iris.model.
+
+Module ModelTest. (* Make sure we got the notations right. *)
+  Definition iResTest (Σ : iParam) (w : iWld Σ) (p : iPst Σ) (g : iGst Σ) : iRes Σ := Res w p g.
+End ModelTest.