diff --git a/_CoqProject b/_CoqProject
index 5cd928c73d0464b51d3dcf3c7f1e4e0b45412e4e..7f6a715d45701c7e3f2591b9ca9486349a8984da 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -17,13 +17,13 @@ theories/lang/adequacy.v
 theories/lang/heap.v
 theories/lang/lang.v
 theories/lang/lifting.v
-theories/lang/memcpy.v
-theories/lang/new_delete.v
 theories/lang/notation.v
 theories/lang/proofmode.v
 theories/lang/races.v
 theories/lang/tactics.v
-theories/lang/spawn.v
+theories/lang/lib/memcpy.v
+theories/lang/lib/new_delete.v
+theories/lang/lib/spawn.v
 theories/typing/base.v
 theories/typing/type.v
 theories/typing/util.v
diff --git a/theories/lang/memcpy.v b/theories/lang/lib/memcpy.v
similarity index 100%
rename from theories/lang/memcpy.v
rename to theories/lang/lib/memcpy.v
diff --git a/theories/lang/new_delete.v b/theories/lang/lib/new_delete.v
similarity index 100%
rename from theories/lang/new_delete.v
rename to theories/lang/lib/new_delete.v
diff --git a/theories/lang/spawn.v b/theories/lang/lib/spawn.v
similarity index 100%
rename from theories/lang/spawn.v
rename to theories/lang/lib/spawn.v
diff --git a/theories/typing/lib/cell.v b/theories/typing/lib/cell.v
index 023d116ba6ba3e7bd3099e97e026dcfd1938fb3f..9234d7f81d2f93538cf7d7da21b14bea1c1bb207 100644
--- a/theories/typing/lib/cell.v
+++ b/theories/typing/lib/cell.v
@@ -1,6 +1,6 @@
 From iris.proofmode Require Import tactics.
 From iris.base_logic Require Import big_op.
-From lrust.lang Require Import memcpy.
+From lrust.lang.lib Require Import memcpy.
 From lrust.lifetime Require Import na_borrow.
 From lrust.typing Require Export type.
 From lrust.typing Require Import typing.
diff --git a/theories/typing/lib/rc.v b/theories/typing/lib/rc.v
index 4f67aa131ae9459c8549489aa49d081803ea407b..a3ede2cf96eb2e8ed1d6e02efee72379ef32ff10 100644
--- a/theories/typing/lib/rc.v
+++ b/theories/typing/lib/rc.v
@@ -2,7 +2,7 @@ From Coq.QArith Require Import Qcanon.
 From iris.proofmode Require Import tactics.
 From iris.algebra Require Import auth csum frac agree.
 From iris.base_logic Require Import big_op.
-From lrust.lang Require Import memcpy.
+From lrust.lang.lib Require Import memcpy.
 From lrust.lifetime Require Import na_borrow.
 From lrust.typing Require Export type.
 From lrust.typing Require Import typing option.
diff --git a/theories/typing/lib/refcell/refcell_code.v b/theories/typing/lib/refcell/refcell_code.v
index fcea5370e14fb2cbd500e6cfa8f2a312e9659f2b..b68b7e895fb50288c8af0cc68e8d17c419125224 100644
--- a/theories/typing/lib/refcell/refcell_code.v
+++ b/theories/typing/lib/refcell/refcell_code.v
@@ -2,7 +2,7 @@ From Coq.QArith Require Import Qcanon.
 From iris.proofmode Require Import tactics.
 From iris.algebra Require Import auth csum frac agree.
 From iris.base_logic Require Import big_op fractional.
-From lrust.lang Require Import memcpy.
+From lrust.lang.lib Require Import memcpy.
 From lrust.lifetime Require Import na_borrow.
 From lrust.typing Require Import typing option.
 From lrust.typing.lib.refcell Require Import refcell ref refmut.
diff --git a/theories/typing/lib/rwlock/rwlock_code.v b/theories/typing/lib/rwlock/rwlock_code.v
index a82f950b028c05a9d1e79389cd42cefde77d92ec..1d81abac2c64e177ada4074cb4f961d67f4dc46f 100644
--- a/theories/typing/lib/rwlock/rwlock_code.v
+++ b/theories/typing/lib/rwlock/rwlock_code.v
@@ -2,7 +2,7 @@ From Coq.QArith Require Import Qcanon.
 From iris.proofmode Require Import tactics.
 From iris.algebra Require Import auth csum frac agree.
 From iris.base_logic Require Import big_op fractional.
-From lrust.lang Require Import memcpy.
+From lrust.lang.lib Require Import memcpy.
 From lrust.lifetime Require Import na_borrow.
 From lrust.typing Require Import typing option.
 From lrust.typing.lib.rwlock Require Import rwlock rwlockreadguard rwlockwriteguard.
diff --git a/theories/typing/own.v b/theories/typing/own.v
index 5268ca3863702f385210f2ce42490c5d3f49eba8..f023f1e48d47f99bf631c8effb91e8bda70a7e51 100644
--- a/theories/typing/own.v
+++ b/theories/typing/own.v
@@ -1,8 +1,7 @@
 From Coq Require Import Qcanon.
 From iris.proofmode Require Import tactics.
 From iris.base_logic Require Import big_op.
-From lrust.lang Require Export new_delete.
-From lrust.lang Require Import memcpy.
+From lrust.lang.lib Require Import new_delete memcpy.
 From lrust.typing Require Export type.
 From lrust.typing Require Import util uninit type_context programs.
 Set Default Proof Using "Type".