diff --git a/_CoqProject b/_CoqProject
index 77a40ad54ffbdfb45cac34eb2883775a341f0c4b..5baef5ecebc5dfd9f1cc17ce23cdaac279f46dde 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -1,4 +1,4 @@
--Q theories actris
+-Q actris actris
 -Q multi_actris multi_actris
 # We sometimes want to locally override notation, and there is no good way to do that with scopes.
 -arg -w -arg -notation-overridden
@@ -6,51 +6,51 @@
 # (https://github.com/coq/coq/issues/6294).
 -arg -w -arg -redundant-canonical-projection
 
-theories/utils/llist.v
-theories/utils/compare.v
-theories/utils/contribution.v
-theories/utils/group.v
-theories/utils/cofe_solver_2.v
-theories/utils/switch.v
-theories/channel/proto_model.v
-theories/channel/proto.v
-theories/channel/channel.v
-theories/channel/proofmode.v
-theories/examples/basics.v
-theories/examples/equivalence.v
-theories/examples/sort.v
-theories/examples/sort_br_del.v
-theories/examples/sort_fg.v
-theories/examples/par_map.v
-theories/examples/map_reduce.v
-theories/examples/swap_mapper.v
-theories/examples/subprotocols.v
-theories/examples/list_rev.v
-theories/examples/rpc.v
-theories/examples/pizza.v
-theories/logrel/model.v
-theories/logrel/telescopes.v
-theories/logrel/subtyping.v
-theories/logrel/contexts.v
-theories/logrel/term_types.v
-theories/logrel/session_types.v
-theories/logrel/operators.v
-theories/logrel/term_typing_judgment.v
-theories/logrel/subtyping_rules.v
-theories/logrel/term_typing_rules.v
-theories/logrel/session_typing_rules.v
-theories/logrel/napp.v
-theories/logrel/lib/mutex.v
-theories/logrel/lib/list.v
-theories/logrel/lib/par_start.v
-theories/logrel/examples/pair.v
-theories/logrel/examples/par_recv.v
-theories/logrel/examples/rec_subtyping.v
-theories/logrel/examples/choice_subtyping.v
-theories/logrel/examples/mapper.v
-theories/logrel/examples/mapper_list.v
-theories/logrel/examples/compute_service.v
-theories/logrel/examples/compute_client_list.v
+actris/utils/llist.v
+actris/utils/compare.v
+actris/utils/contribution.v
+actris/utils/group.v
+actris/utils/cofe_solver_2.v
+actris/utils/switch.v
+actris/channel/proto_model.v
+actris/channel/proto.v
+actris/channel/channel.v
+actris/channel/proofmode.v
+actris/examples/basics.v
+actris/examples/equivalence.v
+actris/examples/sort.v
+actris/examples/sort_br_del.v
+actris/examples/sort_fg.v
+actris/examples/par_map.v
+actris/examples/map_reduce.v
+actris/examples/swap_mapper.v
+actris/examples/subprotocols.v
+actris/examples/list_rev.v
+actris/examples/rpc.v
+actris/examples/pizza.v
+actris/logrel/model.v
+actris/logrel/telescopes.v
+actris/logrel/subtyping.v
+actris/logrel/contexts.v
+actris/logrel/term_types.v
+actris/logrel/session_types.v
+actris/logrel/operators.v
+actris/logrel/term_typing_judgment.v
+actris/logrel/subtyping_rules.v
+actris/logrel/term_typing_rules.v
+actris/logrel/session_typing_rules.v
+actris/logrel/napp.v
+actris/logrel/lib/mutex.v
+actris/logrel/lib/list.v
+actris/logrel/lib/par_start.v
+actris/logrel/examples/pair.v
+actris/logrel/examples/par_recv.v
+actris/logrel/examples/rec_subtyping.v
+actris/logrel/examples/choice_subtyping.v
+actris/logrel/examples/mapper.v
+actris/logrel/examples/mapper_list.v
+actris/logrel/examples/compute_service.v
+actris/logrel/examples/compute_client_list.v
 
 multi_actris/utils/cofe_solver_2.v
 multi_actris/utils/matrix.v
diff --git a/theories/channel/channel.v b/actris/channel/channel.v
similarity index 100%
rename from theories/channel/channel.v
rename to actris/channel/channel.v
diff --git a/theories/channel/proofmode.v b/actris/channel/proofmode.v
similarity index 100%
rename from theories/channel/proofmode.v
rename to actris/channel/proofmode.v
diff --git a/theories/channel/proto.v b/actris/channel/proto.v
similarity index 100%
rename from theories/channel/proto.v
rename to actris/channel/proto.v
diff --git a/theories/channel/proto_model.v b/actris/channel/proto_model.v
similarity index 100%
rename from theories/channel/proto_model.v
rename to actris/channel/proto_model.v
diff --git a/theories/examples/basics.v b/actris/examples/basics.v
similarity index 100%
rename from theories/examples/basics.v
rename to actris/examples/basics.v
diff --git a/theories/examples/equivalence.v b/actris/examples/equivalence.v
similarity index 100%
rename from theories/examples/equivalence.v
rename to actris/examples/equivalence.v
diff --git a/theories/examples/list_rev.v b/actris/examples/list_rev.v
similarity index 100%
rename from theories/examples/list_rev.v
rename to actris/examples/list_rev.v
diff --git a/theories/examples/map_reduce.v b/actris/examples/map_reduce.v
similarity index 100%
rename from theories/examples/map_reduce.v
rename to actris/examples/map_reduce.v
diff --git a/theories/examples/par_map.v b/actris/examples/par_map.v
similarity index 100%
rename from theories/examples/par_map.v
rename to actris/examples/par_map.v
diff --git a/theories/examples/pizza.v b/actris/examples/pizza.v
similarity index 100%
rename from theories/examples/pizza.v
rename to actris/examples/pizza.v
diff --git a/theories/examples/rpc.v b/actris/examples/rpc.v
similarity index 100%
rename from theories/examples/rpc.v
rename to actris/examples/rpc.v
diff --git a/theories/examples/sort.v b/actris/examples/sort.v
similarity index 100%
rename from theories/examples/sort.v
rename to actris/examples/sort.v
diff --git a/theories/examples/sort_br_del.v b/actris/examples/sort_br_del.v
similarity index 100%
rename from theories/examples/sort_br_del.v
rename to actris/examples/sort_br_del.v
diff --git a/theories/examples/sort_fg.v b/actris/examples/sort_fg.v
similarity index 100%
rename from theories/examples/sort_fg.v
rename to actris/examples/sort_fg.v
diff --git a/theories/examples/subprotocols.v b/actris/examples/subprotocols.v
similarity index 100%
rename from theories/examples/subprotocols.v
rename to actris/examples/subprotocols.v
diff --git a/theories/examples/swap_mapper.v b/actris/examples/swap_mapper.v
similarity index 100%
rename from theories/examples/swap_mapper.v
rename to actris/examples/swap_mapper.v
diff --git a/theories/logrel/contexts.v b/actris/logrel/contexts.v
similarity index 100%
rename from theories/logrel/contexts.v
rename to actris/logrel/contexts.v
diff --git a/theories/logrel/examples/choice_subtyping.v b/actris/logrel/examples/choice_subtyping.v
similarity index 100%
rename from theories/logrel/examples/choice_subtyping.v
rename to actris/logrel/examples/choice_subtyping.v
diff --git a/theories/logrel/examples/compute_client_list.v b/actris/logrel/examples/compute_client_list.v
similarity index 100%
rename from theories/logrel/examples/compute_client_list.v
rename to actris/logrel/examples/compute_client_list.v
diff --git a/theories/logrel/examples/compute_service.v b/actris/logrel/examples/compute_service.v
similarity index 100%
rename from theories/logrel/examples/compute_service.v
rename to actris/logrel/examples/compute_service.v
diff --git a/theories/logrel/examples/mapper.v b/actris/logrel/examples/mapper.v
similarity index 100%
rename from theories/logrel/examples/mapper.v
rename to actris/logrel/examples/mapper.v
diff --git a/theories/logrel/examples/mapper_list.v b/actris/logrel/examples/mapper_list.v
similarity index 100%
rename from theories/logrel/examples/mapper_list.v
rename to actris/logrel/examples/mapper_list.v
diff --git a/theories/logrel/examples/pair.v b/actris/logrel/examples/pair.v
similarity index 100%
rename from theories/logrel/examples/pair.v
rename to actris/logrel/examples/pair.v
diff --git a/theories/logrel/examples/par_recv.v b/actris/logrel/examples/par_recv.v
similarity index 100%
rename from theories/logrel/examples/par_recv.v
rename to actris/logrel/examples/par_recv.v
diff --git a/theories/logrel/examples/rec_subtyping.v b/actris/logrel/examples/rec_subtyping.v
similarity index 100%
rename from theories/logrel/examples/rec_subtyping.v
rename to actris/logrel/examples/rec_subtyping.v
diff --git a/theories/logrel/lib/list.v b/actris/logrel/lib/list.v
similarity index 100%
rename from theories/logrel/lib/list.v
rename to actris/logrel/lib/list.v
diff --git a/theories/logrel/lib/mutex.v b/actris/logrel/lib/mutex.v
similarity index 100%
rename from theories/logrel/lib/mutex.v
rename to actris/logrel/lib/mutex.v
diff --git a/theories/logrel/lib/par_start.v b/actris/logrel/lib/par_start.v
similarity index 100%
rename from theories/logrel/lib/par_start.v
rename to actris/logrel/lib/par_start.v
diff --git a/theories/logrel/model.v b/actris/logrel/model.v
similarity index 100%
rename from theories/logrel/model.v
rename to actris/logrel/model.v
diff --git a/theories/logrel/napp.v b/actris/logrel/napp.v
similarity index 100%
rename from theories/logrel/napp.v
rename to actris/logrel/napp.v
diff --git a/theories/logrel/operators.v b/actris/logrel/operators.v
similarity index 100%
rename from theories/logrel/operators.v
rename to actris/logrel/operators.v
diff --git a/theories/logrel/session_types.v b/actris/logrel/session_types.v
similarity index 100%
rename from theories/logrel/session_types.v
rename to actris/logrel/session_types.v
diff --git a/theories/logrel/session_typing_rules.v b/actris/logrel/session_typing_rules.v
similarity index 100%
rename from theories/logrel/session_typing_rules.v
rename to actris/logrel/session_typing_rules.v
diff --git a/theories/logrel/subtyping.v b/actris/logrel/subtyping.v
similarity index 100%
rename from theories/logrel/subtyping.v
rename to actris/logrel/subtyping.v
diff --git a/theories/logrel/subtyping_rules.v b/actris/logrel/subtyping_rules.v
similarity index 100%
rename from theories/logrel/subtyping_rules.v
rename to actris/logrel/subtyping_rules.v
diff --git a/theories/logrel/telescopes.v b/actris/logrel/telescopes.v
similarity index 100%
rename from theories/logrel/telescopes.v
rename to actris/logrel/telescopes.v
diff --git a/theories/logrel/term_types.v b/actris/logrel/term_types.v
similarity index 100%
rename from theories/logrel/term_types.v
rename to actris/logrel/term_types.v
diff --git a/theories/logrel/term_typing_judgment.v b/actris/logrel/term_typing_judgment.v
similarity index 100%
rename from theories/logrel/term_typing_judgment.v
rename to actris/logrel/term_typing_judgment.v
diff --git a/theories/logrel/term_typing_rules.v b/actris/logrel/term_typing_rules.v
similarity index 100%
rename from theories/logrel/term_typing_rules.v
rename to actris/logrel/term_typing_rules.v
diff --git a/theories/utils/cofe_solver_2.v b/actris/utils/cofe_solver_2.v
similarity index 100%
rename from theories/utils/cofe_solver_2.v
rename to actris/utils/cofe_solver_2.v
diff --git a/theories/utils/compare.v b/actris/utils/compare.v
similarity index 100%
rename from theories/utils/compare.v
rename to actris/utils/compare.v
diff --git a/theories/utils/contribution.v b/actris/utils/contribution.v
similarity index 100%
rename from theories/utils/contribution.v
rename to actris/utils/contribution.v
diff --git a/theories/utils/group.v b/actris/utils/group.v
similarity index 100%
rename from theories/utils/group.v
rename to actris/utils/group.v
diff --git a/theories/utils/llist.v b/actris/utils/llist.v
similarity index 100%
rename from theories/utils/llist.v
rename to actris/utils/llist.v
diff --git a/theories/utils/switch.v b/actris/utils/switch.v
similarity index 100%
rename from theories/utils/switch.v
rename to actris/utils/switch.v
diff --git a/coq-actris.opam b/coq-actris.opam
index 0f0153afb1d1c9ef7fc76cdd2870f19ced3da274..c94b261865047855963029dcb7945d0c1f5f420e 100644
--- a/coq-actris.opam
+++ b/coq-actris.opam
@@ -11,5 +11,5 @@ depends: [
   "coq-iris-heap-lang" { (= "dev.2024-10-30.0.27f837c1") | (= "dev") }
 ]
 
-build: [make "-j%{jobs}%"]
-install: [make "install"]
+build: ["./make-package" "actris" "-j%{jobs}%"]
+install: ["./make-package" "actris"  "install"]
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"*