diff --git a/theories/typing/typing.v b/theories/typing/typing.v
new file mode 100644
index 0000000000000000000000000000000000000000..cdbc2552da4b4e7fd60dec80bceaaf673e24b10a
--- /dev/null
+++ b/theories/typing/typing.v
@@ -0,0 +1,9 @@
+From lrust.lang Require Export tactics memcpy notation.
+From lrust.typing Require Export
+  lft_contexts type_context cont_context programs cont type
+  int bool own uniq_bor shr_bor uninit product sum fixpoint function
+  product_split borrow type_sum.
+
+(* Last, so that we make sure we shadow the defintion of delete for
+   collections coming from the prelude. *)
+From lrust.lang Require Export new_delete.