diff --git a/README.md b/README.md
index 6e160a662165b10b0566eaeb02f2a3132c1870b0..4b73aab77e47abe1504278d5a29366b5583423ae 100644
--- a/README.md
+++ b/README.md
@@ -35,10 +35,14 @@ running:
 * The folder `program_logic` builds the semantic domain of Iris, defines and
   verifies primitive view shifts and weakest preconditions, and builds some
   language-independent derived constructions (e.g., STSs).
-* The folder `heap_lang` defines the ML-like concurrent heap language, and a
-  few derived constructions (e.g., parallel composition).
-* The folder `barrier` contains the implementation and proof of the barrier
-  <http://doi.acm.org/10.1145/2818638>.
+* The folder `heap_lang` defines the ML-like concurrent heap language
+  * The subfolder `lib` contains a few derived constructions within this
+    language, e.g., parallel composition.
+    Most notable here s `lib/barrier`, the implementation and proof of a barrier
+    as described in <http://doi.acm.org/10.1145/2818638>.
+* The folder `tests` contains modules we use to test our infrastructure.
+  Users of the Iris Coq library should *not* depend on these modules; they may
+  change or disappear without any notice.
 
 ## Documentation
 
diff --git a/_CoqProject b/_CoqProject
index 0cbaa47d1b3be5abaffccb25e7678c59568ee95c..e3074c433b294bf52f93d2ddf2a52b69fd4b5baa 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -69,7 +69,6 @@ program_logic/pviewshifts.v
 program_logic/resources.v
 program_logic/hoare.v
 program_logic/language.v
-program_logic/tests.v
 program_logic/ghost_ownership.v
 program_logic/global_functor.v
 program_logic/saved_prop.v
@@ -83,15 +82,16 @@ heap_lang/tactics.v
 heap_lang/wp_tactics.v
 heap_lang/lifting.v
 heap_lang/derived.v
-heap_lang/heap.v
 heap_lang/notation.v
-heap_lang/spawn.v
-heap_lang/par.v
-heap_lang/tests.v
 heap_lang/substitution.v
-heap_lang/assert.v
-barrier/barrier.v
-barrier/specification.v
-barrier/protocol.v
-barrier/proof.v
-barrier/client.v
+heap_lang/lib/heap.v
+heap_lang/lib/spawn.v
+heap_lang/lib/par.v
+heap_lang/lib/assert.v
+heap_lang/lib/barrier/barrier.v
+heap_lang/lib/barrier/specification.v
+heap_lang/lib/barrier/protocol.v
+heap_lang/lib/barrier/proof.v
+heap_lang/lib/barrier/client.v
+tests/heap_lang.v
+tests/program_logic.v
diff --git a/heap_lang/assert.v b/heap_lang/lib/assert.v
similarity index 100%
rename from heap_lang/assert.v
rename to heap_lang/lib/assert.v
diff --git a/barrier/barrier.v b/heap_lang/lib/barrier/barrier.v
similarity index 100%
rename from barrier/barrier.v
rename to heap_lang/lib/barrier/barrier.v
diff --git a/barrier/client.v b/heap_lang/lib/barrier/client.v
similarity index 98%
rename from barrier/client.v
rename to heap_lang/lib/barrier/client.v
index e68492fb9070d15d35fe41010bfa1f8f1ba90d0e..cf2bd60a38b8c7b067bf6a1f40f4c6cccc0c96ca 100644
--- a/barrier/client.v
+++ b/heap_lang/lib/barrier/client.v
@@ -1,4 +1,4 @@
-From iris.barrier Require Import proof.
+From iris.heap_lang.lib.barrier Require Import proof.
 From iris.heap_lang Require Import par.
 From iris.program_logic Require Import auth sts saved_prop hoare ownership.
 Import uPred.
diff --git a/barrier/proof.v b/heap_lang/lib/barrier/proof.v
similarity index 99%
rename from barrier/proof.v
rename to heap_lang/lib/barrier/proof.v
index b0c745823fb1dc38b00e301217f0c7ad9ba4cdef..6ca5d83724173c27fdc92e93354c0907515418fb 100644
--- a/barrier/proof.v
+++ b/heap_lang/lib/barrier/proof.v
@@ -2,8 +2,8 @@ From iris.prelude Require Import functions.
 From iris.algebra Require Import upred_big_op.
 From iris.program_logic Require Import sts saved_prop tactics.
 From iris.heap_lang Require Export heap wp_tactics.
-From iris.barrier Require Export barrier.
-From iris.barrier Require Import protocol.
+From iris.heap_lang.lib.barrier Require Export barrier.
+From iris.heap_lang.lib.barrier Require Import protocol.
 Import uPred.
 
 (** The CMRAs we need. *)
diff --git a/barrier/protocol.v b/heap_lang/lib/barrier/protocol.v
similarity index 100%
rename from barrier/protocol.v
rename to heap_lang/lib/barrier/protocol.v
diff --git a/barrier/specification.v b/heap_lang/lib/barrier/specification.v
similarity index 92%
rename from barrier/specification.v
rename to heap_lang/lib/barrier/specification.v
index 68631962e4e5ceb4d0e43bfd3845d59bbd8df56c..bfe830080583677713e8d554158ff7ec04550887 100644
--- a/barrier/specification.v
+++ b/heap_lang/lib/barrier/specification.v
@@ -1,6 +1,6 @@
 From iris.program_logic Require Export hoare.
-From iris.barrier Require Export barrier.
-From iris.barrier Require Import proof.
+From iris.heap_lang.lib.barrier Require Export barrier.
+From iris.heap_lang.lib.barrier Require Import proof.
 Import uPred.
 
 Section spec.
diff --git a/heap_lang/heap.v b/heap_lang/lib/heap.v
similarity index 100%
rename from heap_lang/heap.v
rename to heap_lang/lib/heap.v
diff --git a/heap_lang/par.v b/heap_lang/lib/par.v
similarity index 100%
rename from heap_lang/par.v
rename to heap_lang/lib/par.v
diff --git a/heap_lang/spawn.v b/heap_lang/lib/spawn.v
similarity index 100%
rename from heap_lang/spawn.v
rename to heap_lang/lib/spawn.v
diff --git a/heap_lang/tests.v b/tests/heap_lang.v
similarity index 100%
rename from heap_lang/tests.v
rename to tests/heap_lang.v
diff --git a/program_logic/tests.v b/tests/program_logic.v
similarity index 100%
rename from program_logic/tests.v
rename to tests/program_logic.v