diff --git a/_CoqProject b/_CoqProject
index 388e1c6792f003b7f7cd9aec56c16854b2483023..8a8ef0b08a202d7e2a222d400b22a7e5008e84d7 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -1,94 +1,98 @@
--Q theories lrust
+# Search paths for all packages. They must all match the regex
+# `-Q $PACKAGE[/ ]` so that we can filter out the right ones for each package.
+-Q lifetime lrust.lifetime
+-Q lambda-rust/lang lrust.lang
+-Q lambda-rust/typing lrust.typing
 # We sometimes want to locally override notation, and there is no good way to do that with scopes.
 -arg -w -arg -notation-overridden
 # Cannot use non-canonical projections as it causes massive unification failures
 # (https://github.com/coq/coq/issues/6294).
 -arg -w -arg -redundant-canonical-projection
 
-theories/lifetime/model/definitions.v
-theories/lifetime/model/faking.v
-theories/lifetime/model/creation.v
-theories/lifetime/model/primitive.v
-theories/lifetime/model/accessors.v
-theories/lifetime/model/borrow.v
-theories/lifetime/model/borrow_sep.v
-theories/lifetime/model/reborrow.v
-theories/lifetime/lifetime_sig.v
-theories/lifetime/lifetime.v
-theories/lifetime/at_borrow.v
-theories/lifetime/na_borrow.v
-theories/lifetime/frac_borrow.v
-theories/lifetime/meta.v
-theories/lang/adequacy.v
-theories/lang/heap.v
-theories/lang/lang.v
-theories/lang/lifting.v
-theories/lang/notation.v
-theories/lang/proofmode.v
-theories/lang/races.v
-theories/lang/tactics.v
-theories/lang/lib/memcpy.v
-theories/lang/lib/swap.v
-theories/lang/lib/new_delete.v
-theories/lang/lib/spawn.v
-theories/lang/lib/lock.v
-theories/lang/lib/arc.v
-theories/lang/lib/tests.v
-theories/typing/base.v
-theories/typing/type.v
-theories/typing/util.v
-theories/typing/lft_contexts.v
-theories/typing/type_context.v
-theories/typing/cont_context.v
-theories/typing/uninit.v
-theories/typing/own.v
-theories/typing/uniq_bor.v
-theories/typing/shr_bor.v
-theories/typing/product.v
-theories/typing/product_split.v
-theories/typing/sum.v
-theories/typing/bool.v
-theories/typing/int.v
-theories/typing/function.v
-theories/typing/programs.v
-theories/typing/borrow.v
-theories/typing/cont.v
-theories/typing/fixpoint.v
-theories/typing/type_sum.v
-theories/typing/typing.v
-theories/typing/soundness.v
-theories/typing/lib/panic.v
-theories/typing/lib/option.v
-theories/typing/lib/fake_shared.v
-theories/typing/lib/cell.v
-theories/typing/lib/spawn.v
-theories/typing/lib/join.v
-theories/typing/lib/take_mut.v
-theories/typing/lib/rc/rc.v
-theories/typing/lib/rc/weak.v
-theories/typing/lib/arc.v
-theories/typing/lib/swap.v
-theories/typing/lib/diverging_static.v
-theories/typing/lib/brandedvec.v
-theories/typing/lib/ghostcell.v
-theories/typing/lib/mutex/mutex.v
-theories/typing/lib/mutex/mutexguard.v
-theories/typing/lib/refcell/refcell.v
-theories/typing/lib/refcell/ref.v
-theories/typing/lib/refcell/refmut.v
-theories/typing/lib/refcell/refcell_code.v
-theories/typing/lib/refcell/ref_code.v
-theories/typing/lib/refcell/refmut_code.v
-theories/typing/lib/rwlock/rwlock.v
-theories/typing/lib/rwlock/rwlockreadguard.v
-theories/typing/lib/rwlock/rwlockwriteguard.v
-theories/typing/lib/rwlock/rwlock_code.v
-theories/typing/lib/rwlock/rwlockreadguard_code.v
-theories/typing/lib/rwlock/rwlockwriteguard_code.v
-theories/typing/examples/fixpoint.v
-theories/typing/examples/get_x.v
-theories/typing/examples/rebor.v
-theories/typing/examples/unbox.v
-theories/typing/examples/init_prod.v
-theories/typing/examples/lazy_lft.v
-theories/typing/examples/nonlexical.v
+lifetime/model/definitions.v
+lifetime/model/faking.v
+lifetime/model/creation.v
+lifetime/model/primitive.v
+lifetime/model/accessors.v
+lifetime/model/borrow.v
+lifetime/model/borrow_sep.v
+lifetime/model/reborrow.v
+lifetime/lifetime_sig.v
+lifetime/lifetime.v
+lifetime/at_borrow.v
+lifetime/na_borrow.v
+lifetime/frac_borrow.v
+lifetime/meta.v
+lambda-rust/lang/adequacy.v
+lambda-rust/lang/heap.v
+lambda-rust/lang/lang.v
+lambda-rust/lang/lifting.v
+lambda-rust/lang/notation.v
+lambda-rust/lang/proofmode.v
+lambda-rust/lang/races.v
+lambda-rust/lang/tactics.v
+lambda-rust/lang/lib/memcpy.v
+lambda-rust/lang/lib/swap.v
+lambda-rust/lang/lib/new_delete.v
+lambda-rust/lang/lib/spawn.v
+lambda-rust/lang/lib/lock.v
+lambda-rust/lang/lib/arc.v
+lambda-rust/lang/lib/tests.v
+lambda-rust/typing/base.v
+lambda-rust/typing/type.v
+lambda-rust/typing/util.v
+lambda-rust/typing/lft_contexts.v
+lambda-rust/typing/type_context.v
+lambda-rust/typing/cont_context.v
+lambda-rust/typing/uninit.v
+lambda-rust/typing/own.v
+lambda-rust/typing/uniq_bor.v
+lambda-rust/typing/shr_bor.v
+lambda-rust/typing/product.v
+lambda-rust/typing/product_split.v
+lambda-rust/typing/sum.v
+lambda-rust/typing/bool.v
+lambda-rust/typing/int.v
+lambda-rust/typing/function.v
+lambda-rust/typing/programs.v
+lambda-rust/typing/borrow.v
+lambda-rust/typing/cont.v
+lambda-rust/typing/fixpoint.v
+lambda-rust/typing/type_sum.v
+lambda-rust/typing/typing.v
+lambda-rust/typing/soundness.v
+lambda-rust/typing/lib/panic.v
+lambda-rust/typing/lib/option.v
+lambda-rust/typing/lib/fake_shared.v
+lambda-rust/typing/lib/cell.v
+lambda-rust/typing/lib/spawn.v
+lambda-rust/typing/lib/join.v
+lambda-rust/typing/lib/take_mut.v
+lambda-rust/typing/lib/rc/rc.v
+lambda-rust/typing/lib/rc/weak.v
+lambda-rust/typing/lib/arc.v
+lambda-rust/typing/lib/swap.v
+lambda-rust/typing/lib/diverging_static.v
+lambda-rust/typing/lib/brandedvec.v
+lambda-rust/typing/lib/ghostcell.v
+lambda-rust/typing/lib/mutex/mutex.v
+lambda-rust/typing/lib/mutex/mutexguard.v
+lambda-rust/typing/lib/refcell/refcell.v
+lambda-rust/typing/lib/refcell/ref.v
+lambda-rust/typing/lib/refcell/refmut.v
+lambda-rust/typing/lib/refcell/refcell_code.v
+lambda-rust/typing/lib/refcell/ref_code.v
+lambda-rust/typing/lib/refcell/refmut_code.v
+lambda-rust/typing/lib/rwlock/rwlock.v
+lambda-rust/typing/lib/rwlock/rwlockreadguard.v
+lambda-rust/typing/lib/rwlock/rwlockwriteguard.v
+lambda-rust/typing/lib/rwlock/rwlock_code.v
+lambda-rust/typing/lib/rwlock/rwlockreadguard_code.v
+lambda-rust/typing/lib/rwlock/rwlockwriteguard_code.v
+lambda-rust/typing/examples/fixpoint.v
+lambda-rust/typing/examples/get_x.v
+lambda-rust/typing/examples/rebor.v
+lambda-rust/typing/examples/unbox.v
+lambda-rust/typing/examples/init_prod.v
+lambda-rust/typing/examples/lazy_lft.v
+lambda-rust/typing/examples/nonlexical.v
diff --git a/coq-lambda-rust.opam b/coq-lambda-rust.opam
index 1120df37d63dea894022dff37cb9d1fe6eb7fa69..cb1a9b4d59def0021733b64107c246a16f7ffa77 100644
--- a/coq-lambda-rust.opam
+++ b/coq-lambda-rust.opam
@@ -13,8 +13,8 @@ the type system, and safety proof for some Rust libraries.
 """
 
 depends: [
-  "coq-iris" { (= "dev.2024-02-16.1.06f499e0") | (= "dev") }
+  "coq-lifetime-logic" { = version }
 ]
 
-build: [make "-j%{jobs}%"]
-install: [make "install"]
+build: ["./make-package" "lambda-rust" "-j%{jobs}%"]
+install: ["./make-package" "lambda-rust" "install"]
diff --git a/coq-lifetime-logic.opam b/coq-lifetime-logic.opam
new file mode 100644
index 0000000000000000000000000000000000000000..accb10e816d5188ca16d447084f95186376b5159
--- /dev/null
+++ b/coq-lifetime-logic.opam
@@ -0,0 +1,19 @@
+opam-version: "2.0"
+maintainer: "Ralf Jung <jung@mpi-sws.org>"
+authors: "The RustBelt Team"
+license: "BSD-3-Clause"
+homepage: "https://plv.mpi-sws.org/rustbelt/"
+bug-reports: "https://gitlab.mpi-sws.org/iris/lambda-rust/issues"
+dev-repo: "git+https://gitlab.mpi-sws.org/iris/lambda-rust.git"
+
+synopsis: "Lifetime Logic Coq formalization"
+description: """
+The lifetime logic extends Iris with a notion of "borrowing".
+"""
+
+depends: [
+  "coq-iris" { (= "dev.2024-03-05.0.d71f4877") | (= "dev") }
+]
+
+build: ["./make-package" "lambda-rust" "-j%{jobs}%"]
+install: ["./make-package" "lambda-rust" "install"]
diff --git a/theories/lang/adequacy.v b/lambda-rust/lang/adequacy.v
similarity index 100%
rename from theories/lang/adequacy.v
rename to lambda-rust/lang/adequacy.v
diff --git a/theories/lang/heap.v b/lambda-rust/lang/heap.v
similarity index 100%
rename from theories/lang/heap.v
rename to lambda-rust/lang/heap.v
diff --git a/theories/lang/lang.v b/lambda-rust/lang/lang.v
similarity index 100%
rename from theories/lang/lang.v
rename to lambda-rust/lang/lang.v
diff --git a/theories/lang/lib/arc.v b/lambda-rust/lang/lib/arc.v
similarity index 100%
rename from theories/lang/lib/arc.v
rename to lambda-rust/lang/lib/arc.v
diff --git a/theories/lang/lib/lock.v b/lambda-rust/lang/lib/lock.v
similarity index 100%
rename from theories/lang/lib/lock.v
rename to lambda-rust/lang/lib/lock.v
diff --git a/theories/lang/lib/memcpy.v b/lambda-rust/lang/lib/memcpy.v
similarity index 100%
rename from theories/lang/lib/memcpy.v
rename to lambda-rust/lang/lib/memcpy.v
diff --git a/theories/lang/lib/new_delete.v b/lambda-rust/lang/lib/new_delete.v
similarity index 100%
rename from theories/lang/lib/new_delete.v
rename to lambda-rust/lang/lib/new_delete.v
diff --git a/theories/lang/lib/spawn.v b/lambda-rust/lang/lib/spawn.v
similarity index 100%
rename from theories/lang/lib/spawn.v
rename to lambda-rust/lang/lib/spawn.v
diff --git a/theories/lang/lib/swap.v b/lambda-rust/lang/lib/swap.v
similarity index 100%
rename from theories/lang/lib/swap.v
rename to lambda-rust/lang/lib/swap.v
diff --git a/theories/lang/lib/tests.v b/lambda-rust/lang/lib/tests.v
similarity index 100%
rename from theories/lang/lib/tests.v
rename to lambda-rust/lang/lib/tests.v
diff --git a/theories/lang/lifting.v b/lambda-rust/lang/lifting.v
similarity index 100%
rename from theories/lang/lifting.v
rename to lambda-rust/lang/lifting.v
diff --git a/theories/lang/notation.v b/lambda-rust/lang/notation.v
similarity index 100%
rename from theories/lang/notation.v
rename to lambda-rust/lang/notation.v
diff --git a/theories/lang/proofmode.v b/lambda-rust/lang/proofmode.v
similarity index 100%
rename from theories/lang/proofmode.v
rename to lambda-rust/lang/proofmode.v
diff --git a/theories/lang/races.v b/lambda-rust/lang/races.v
similarity index 100%
rename from theories/lang/races.v
rename to lambda-rust/lang/races.v
diff --git a/theories/lang/tactics.v b/lambda-rust/lang/tactics.v
similarity index 100%
rename from theories/lang/tactics.v
rename to lambda-rust/lang/tactics.v
diff --git a/theories/typing/base.v b/lambda-rust/typing/base.v
similarity index 100%
rename from theories/typing/base.v
rename to lambda-rust/typing/base.v
diff --git a/theories/typing/bool.v b/lambda-rust/typing/bool.v
similarity index 100%
rename from theories/typing/bool.v
rename to lambda-rust/typing/bool.v
diff --git a/theories/typing/borrow.v b/lambda-rust/typing/borrow.v
similarity index 100%
rename from theories/typing/borrow.v
rename to lambda-rust/typing/borrow.v
diff --git a/theories/typing/cont.v b/lambda-rust/typing/cont.v
similarity index 100%
rename from theories/typing/cont.v
rename to lambda-rust/typing/cont.v
diff --git a/theories/typing/cont_context.v b/lambda-rust/typing/cont_context.v
similarity index 100%
rename from theories/typing/cont_context.v
rename to lambda-rust/typing/cont_context.v
diff --git a/theories/typing/examples/fixpoint.v b/lambda-rust/typing/examples/fixpoint.v
similarity index 100%
rename from theories/typing/examples/fixpoint.v
rename to lambda-rust/typing/examples/fixpoint.v
diff --git a/theories/typing/examples/get_x.v b/lambda-rust/typing/examples/get_x.v
similarity index 100%
rename from theories/typing/examples/get_x.v
rename to lambda-rust/typing/examples/get_x.v
diff --git a/theories/typing/examples/init_prod.v b/lambda-rust/typing/examples/init_prod.v
similarity index 100%
rename from theories/typing/examples/init_prod.v
rename to lambda-rust/typing/examples/init_prod.v
diff --git a/theories/typing/examples/lazy_lft.v b/lambda-rust/typing/examples/lazy_lft.v
similarity index 100%
rename from theories/typing/examples/lazy_lft.v
rename to lambda-rust/typing/examples/lazy_lft.v
diff --git a/theories/typing/examples/nonlexical.v b/lambda-rust/typing/examples/nonlexical.v
similarity index 100%
rename from theories/typing/examples/nonlexical.v
rename to lambda-rust/typing/examples/nonlexical.v
diff --git a/theories/typing/examples/rebor.v b/lambda-rust/typing/examples/rebor.v
similarity index 100%
rename from theories/typing/examples/rebor.v
rename to lambda-rust/typing/examples/rebor.v
diff --git a/theories/typing/examples/unbox.v b/lambda-rust/typing/examples/unbox.v
similarity index 100%
rename from theories/typing/examples/unbox.v
rename to lambda-rust/typing/examples/unbox.v
diff --git a/theories/typing/fixpoint.v b/lambda-rust/typing/fixpoint.v
similarity index 100%
rename from theories/typing/fixpoint.v
rename to lambda-rust/typing/fixpoint.v
diff --git a/theories/typing/function.v b/lambda-rust/typing/function.v
similarity index 100%
rename from theories/typing/function.v
rename to lambda-rust/typing/function.v
diff --git a/theories/typing/int.v b/lambda-rust/typing/int.v
similarity index 100%
rename from theories/typing/int.v
rename to lambda-rust/typing/int.v
diff --git a/theories/typing/lft_contexts.v b/lambda-rust/typing/lft_contexts.v
similarity index 100%
rename from theories/typing/lft_contexts.v
rename to lambda-rust/typing/lft_contexts.v
diff --git a/theories/typing/lib/arc.v b/lambda-rust/typing/lib/arc.v
similarity index 100%
rename from theories/typing/lib/arc.v
rename to lambda-rust/typing/lib/arc.v
diff --git a/theories/typing/lib/brandedvec.v b/lambda-rust/typing/lib/brandedvec.v
similarity index 100%
rename from theories/typing/lib/brandedvec.v
rename to lambda-rust/typing/lib/brandedvec.v
diff --git a/theories/typing/lib/cell.v b/lambda-rust/typing/lib/cell.v
similarity index 100%
rename from theories/typing/lib/cell.v
rename to lambda-rust/typing/lib/cell.v
diff --git a/theories/typing/lib/diverging_static.v b/lambda-rust/typing/lib/diverging_static.v
similarity index 100%
rename from theories/typing/lib/diverging_static.v
rename to lambda-rust/typing/lib/diverging_static.v
diff --git a/theories/typing/lib/fake_shared.v b/lambda-rust/typing/lib/fake_shared.v
similarity index 100%
rename from theories/typing/lib/fake_shared.v
rename to lambda-rust/typing/lib/fake_shared.v
diff --git a/theories/typing/lib/ghostcell.v b/lambda-rust/typing/lib/ghostcell.v
similarity index 100%
rename from theories/typing/lib/ghostcell.v
rename to lambda-rust/typing/lib/ghostcell.v
diff --git a/theories/typing/lib/join.v b/lambda-rust/typing/lib/join.v
similarity index 100%
rename from theories/typing/lib/join.v
rename to lambda-rust/typing/lib/join.v
diff --git a/theories/typing/lib/mutex/mutex.v b/lambda-rust/typing/lib/mutex/mutex.v
similarity index 100%
rename from theories/typing/lib/mutex/mutex.v
rename to lambda-rust/typing/lib/mutex/mutex.v
diff --git a/theories/typing/lib/mutex/mutexguard.v b/lambda-rust/typing/lib/mutex/mutexguard.v
similarity index 100%
rename from theories/typing/lib/mutex/mutexguard.v
rename to lambda-rust/typing/lib/mutex/mutexguard.v
diff --git a/theories/typing/lib/option.v b/lambda-rust/typing/lib/option.v
similarity index 100%
rename from theories/typing/lib/option.v
rename to lambda-rust/typing/lib/option.v
diff --git a/theories/typing/lib/panic.v b/lambda-rust/typing/lib/panic.v
similarity index 100%
rename from theories/typing/lib/panic.v
rename to lambda-rust/typing/lib/panic.v
diff --git a/theories/typing/lib/rc/rc.v b/lambda-rust/typing/lib/rc/rc.v
similarity index 100%
rename from theories/typing/lib/rc/rc.v
rename to lambda-rust/typing/lib/rc/rc.v
diff --git a/theories/typing/lib/rc/weak.v b/lambda-rust/typing/lib/rc/weak.v
similarity index 100%
rename from theories/typing/lib/rc/weak.v
rename to lambda-rust/typing/lib/rc/weak.v
diff --git a/theories/typing/lib/refcell/ref.v b/lambda-rust/typing/lib/refcell/ref.v
similarity index 100%
rename from theories/typing/lib/refcell/ref.v
rename to lambda-rust/typing/lib/refcell/ref.v
diff --git a/theories/typing/lib/refcell/ref_code.v b/lambda-rust/typing/lib/refcell/ref_code.v
similarity index 100%
rename from theories/typing/lib/refcell/ref_code.v
rename to lambda-rust/typing/lib/refcell/ref_code.v
diff --git a/theories/typing/lib/refcell/refcell.v b/lambda-rust/typing/lib/refcell/refcell.v
similarity index 100%
rename from theories/typing/lib/refcell/refcell.v
rename to lambda-rust/typing/lib/refcell/refcell.v
diff --git a/theories/typing/lib/refcell/refcell_code.v b/lambda-rust/typing/lib/refcell/refcell_code.v
similarity index 100%
rename from theories/typing/lib/refcell/refcell_code.v
rename to lambda-rust/typing/lib/refcell/refcell_code.v
diff --git a/theories/typing/lib/refcell/refmut.v b/lambda-rust/typing/lib/refcell/refmut.v
similarity index 100%
rename from theories/typing/lib/refcell/refmut.v
rename to lambda-rust/typing/lib/refcell/refmut.v
diff --git a/theories/typing/lib/refcell/refmut_code.v b/lambda-rust/typing/lib/refcell/refmut_code.v
similarity index 100%
rename from theories/typing/lib/refcell/refmut_code.v
rename to lambda-rust/typing/lib/refcell/refmut_code.v
diff --git a/theories/typing/lib/rwlock/rwlock.v b/lambda-rust/typing/lib/rwlock/rwlock.v
similarity index 100%
rename from theories/typing/lib/rwlock/rwlock.v
rename to lambda-rust/typing/lib/rwlock/rwlock.v
diff --git a/theories/typing/lib/rwlock/rwlock_code.v b/lambda-rust/typing/lib/rwlock/rwlock_code.v
similarity index 100%
rename from theories/typing/lib/rwlock/rwlock_code.v
rename to lambda-rust/typing/lib/rwlock/rwlock_code.v
diff --git a/theories/typing/lib/rwlock/rwlockreadguard.v b/lambda-rust/typing/lib/rwlock/rwlockreadguard.v
similarity index 100%
rename from theories/typing/lib/rwlock/rwlockreadguard.v
rename to lambda-rust/typing/lib/rwlock/rwlockreadguard.v
diff --git a/theories/typing/lib/rwlock/rwlockreadguard_code.v b/lambda-rust/typing/lib/rwlock/rwlockreadguard_code.v
similarity index 100%
rename from theories/typing/lib/rwlock/rwlockreadguard_code.v
rename to lambda-rust/typing/lib/rwlock/rwlockreadguard_code.v
diff --git a/theories/typing/lib/rwlock/rwlockwriteguard.v b/lambda-rust/typing/lib/rwlock/rwlockwriteguard.v
similarity index 100%
rename from theories/typing/lib/rwlock/rwlockwriteguard.v
rename to lambda-rust/typing/lib/rwlock/rwlockwriteguard.v
diff --git a/theories/typing/lib/rwlock/rwlockwriteguard_code.v b/lambda-rust/typing/lib/rwlock/rwlockwriteguard_code.v
similarity index 100%
rename from theories/typing/lib/rwlock/rwlockwriteguard_code.v
rename to lambda-rust/typing/lib/rwlock/rwlockwriteguard_code.v
diff --git a/theories/typing/lib/spawn.v b/lambda-rust/typing/lib/spawn.v
similarity index 100%
rename from theories/typing/lib/spawn.v
rename to lambda-rust/typing/lib/spawn.v
diff --git a/theories/typing/lib/swap.v b/lambda-rust/typing/lib/swap.v
similarity index 100%
rename from theories/typing/lib/swap.v
rename to lambda-rust/typing/lib/swap.v
diff --git a/theories/typing/lib/take_mut.v b/lambda-rust/typing/lib/take_mut.v
similarity index 100%
rename from theories/typing/lib/take_mut.v
rename to lambda-rust/typing/lib/take_mut.v
diff --git a/theories/typing/own.v b/lambda-rust/typing/own.v
similarity index 100%
rename from theories/typing/own.v
rename to lambda-rust/typing/own.v
diff --git a/theories/typing/product.v b/lambda-rust/typing/product.v
similarity index 100%
rename from theories/typing/product.v
rename to lambda-rust/typing/product.v
diff --git a/theories/typing/product_split.v b/lambda-rust/typing/product_split.v
similarity index 100%
rename from theories/typing/product_split.v
rename to lambda-rust/typing/product_split.v
diff --git a/theories/typing/programs.v b/lambda-rust/typing/programs.v
similarity index 100%
rename from theories/typing/programs.v
rename to lambda-rust/typing/programs.v
diff --git a/theories/typing/shr_bor.v b/lambda-rust/typing/shr_bor.v
similarity index 100%
rename from theories/typing/shr_bor.v
rename to lambda-rust/typing/shr_bor.v
diff --git a/theories/typing/soundness.v b/lambda-rust/typing/soundness.v
similarity index 100%
rename from theories/typing/soundness.v
rename to lambda-rust/typing/soundness.v
diff --git a/theories/typing/sum.v b/lambda-rust/typing/sum.v
similarity index 100%
rename from theories/typing/sum.v
rename to lambda-rust/typing/sum.v
diff --git a/theories/typing/type.v b/lambda-rust/typing/type.v
similarity index 100%
rename from theories/typing/type.v
rename to lambda-rust/typing/type.v
diff --git a/theories/typing/type_context.v b/lambda-rust/typing/type_context.v
similarity index 100%
rename from theories/typing/type_context.v
rename to lambda-rust/typing/type_context.v
diff --git a/theories/typing/type_sum.v b/lambda-rust/typing/type_sum.v
similarity index 100%
rename from theories/typing/type_sum.v
rename to lambda-rust/typing/type_sum.v
diff --git a/theories/typing/typing.v b/lambda-rust/typing/typing.v
similarity index 100%
rename from theories/typing/typing.v
rename to lambda-rust/typing/typing.v
diff --git a/theories/typing/uninit.v b/lambda-rust/typing/uninit.v
similarity index 100%
rename from theories/typing/uninit.v
rename to lambda-rust/typing/uninit.v
diff --git a/theories/typing/uniq_bor.v b/lambda-rust/typing/uniq_bor.v
similarity index 100%
rename from theories/typing/uniq_bor.v
rename to lambda-rust/typing/uniq_bor.v
diff --git a/theories/typing/util.v b/lambda-rust/typing/util.v
similarity index 100%
rename from theories/typing/util.v
rename to lambda-rust/typing/util.v
diff --git a/theories/lifetime/at_borrow.v b/lifetime/at_borrow.v
similarity index 100%
rename from theories/lifetime/at_borrow.v
rename to lifetime/at_borrow.v
diff --git a/theories/lifetime/frac_borrow.v b/lifetime/frac_borrow.v
similarity index 100%
rename from theories/lifetime/frac_borrow.v
rename to lifetime/frac_borrow.v
diff --git a/theories/lifetime/lifetime.v b/lifetime/lifetime.v
similarity index 100%
rename from theories/lifetime/lifetime.v
rename to lifetime/lifetime.v
diff --git a/theories/lifetime/lifetime_sig.v b/lifetime/lifetime_sig.v
similarity index 100%
rename from theories/lifetime/lifetime_sig.v
rename to lifetime/lifetime_sig.v
diff --git a/theories/lifetime/meta.v b/lifetime/meta.v
similarity index 100%
rename from theories/lifetime/meta.v
rename to lifetime/meta.v
diff --git a/theories/lifetime/model/accessors.v b/lifetime/model/accessors.v
similarity index 100%
rename from theories/lifetime/model/accessors.v
rename to lifetime/model/accessors.v
diff --git a/theories/lifetime/model/borrow.v b/lifetime/model/borrow.v
similarity index 100%
rename from theories/lifetime/model/borrow.v
rename to lifetime/model/borrow.v
diff --git a/theories/lifetime/model/borrow_sep.v b/lifetime/model/borrow_sep.v
similarity index 100%
rename from theories/lifetime/model/borrow_sep.v
rename to lifetime/model/borrow_sep.v
diff --git a/theories/lifetime/model/creation.v b/lifetime/model/creation.v
similarity index 100%
rename from theories/lifetime/model/creation.v
rename to lifetime/model/creation.v
diff --git a/theories/lifetime/model/definitions.v b/lifetime/model/definitions.v
similarity index 100%
rename from theories/lifetime/model/definitions.v
rename to lifetime/model/definitions.v
diff --git a/theories/lifetime/model/faking.v b/lifetime/model/faking.v
similarity index 100%
rename from theories/lifetime/model/faking.v
rename to lifetime/model/faking.v
diff --git a/theories/lifetime/model/primitive.v b/lifetime/model/primitive.v
similarity index 100%
rename from theories/lifetime/model/primitive.v
rename to lifetime/model/primitive.v
diff --git a/theories/lifetime/model/reborrow.v b/lifetime/model/reborrow.v
similarity index 100%
rename from theories/lifetime/model/reborrow.v
rename to lifetime/model/reborrow.v
diff --git a/theories/lifetime/na_borrow.v b/lifetime/na_borrow.v
similarity index 100%
rename from theories/lifetime/na_borrow.v
rename to lifetime/na_borrow.v
diff --git a/make-package b/make-package
new file mode 100755
index 0000000000000000000000000000000000000000..5bf541bca26c231313c0343bccda663d665c11e9
--- /dev/null
+++ b/make-package
@@ -0,0 +1,32 @@
+#!/bin/bash
+set -e
+# Helper script to build and/or install just one package out of this repository.
+# Assumes that all the other packages it depends on have been installed already!
+
+PROJECT="$1"
+shift
+
+COQFILE="_CoqProject.$PROJECT"
+MAKEFILE="Makefile.package.$PROJECT"
+
+if ! grep -E -q "^$PROJECT/" _CoqProject; then
+    echo "No files in $PROJECT/ found in _CoqProject; this does not seem to be a valid project name."
+    exit 1
+fi
+
+# Generate _CoqProject file and Makefile
+rm -f "$COQFILE"
+# Get the right "-Q" line.
+grep -E "^-Q $PROJECT[ /]" _CoqProject >> "$COQFILE"
+# Get everything until the first empty line except for the "-Q" lines.
+sed -n '/./!q;p' _CoqProject | grep -E -v "^-Q " >> "$COQFILE"
+# Get the files.
+grep -E "^$PROJECT/" _CoqProject >> "$COQFILE"
+# Now we can run coq_makefile.
+"${COQBIN}coq_makefile" -f "$COQFILE" -o "$MAKEFILE"
+
+# Run build
+make -f "$MAKEFILE" "$@"
+
+# Cleanup
+rm -f ".$MAKEFILE.d" "$MAKEFILE"*