diff --git a/coq-lithium.opam b/coq-lithium.opam
index 6d787f7f2773abc186ceb902cb2d782faa222791..0a7468ed2517ccad6c2e1ad54c1e29fdab958534 100644
--- a/coq-lithium.opam
+++ b/coq-lithium.opam
@@ -18,7 +18,7 @@ depends: [
   "coq" { (= "8.17.0" ) }
   "coq-iris" { (= "dev.2023-06-14.0.f0e415b6") | (= "dev") }
   "coq-stdpp-unstable"
-  "dune" {>= "3.0.3"}
+  "dune" {>= "3.9.1"}
   "coq-record-update" {= "0.3.0"}
 ]
 
diff --git a/dune-project b/dune-project
index b506f83c9cd32092fd88f4f0f5d32db1ec02b0c3..08dd966aa8c6f1ebbc964ff1a424c8d9b0fc76d1 100644
--- a/dune-project
+++ b/dune-project
@@ -1,5 +1,5 @@
-(lang dune 2.9)
+(lang dune 3.8)
 (name refinedrust)
 (package (name refinedrust))
 (package (name coq-lithium))
-(using coq 0.3)
+(using coq 0.8)
diff --git a/theories/caesium/config/dune b/theories/caesium/config/dune
index 800df748417394628d1cec47c435482056409993..a930360397b1258e856ec204ff1322b83eff17bb 100644
--- a/theories/caesium/config/dune
+++ b/theories/caesium/config/dune
@@ -3,6 +3,4 @@
  (package refinedrust)
  (flags :standard -w -notation-overridden -w -redundant-canonical-projection)
  (synopsis "Configuration of the Caesium language")
- (theories 
-   ;lithium stdpp iris RecordUpdate Ltac2
-   ))
+ (theories lithium stdpp iris RecordUpdate Ltac2))
diff --git a/theories/caesium/dune b/theories/caesium/dune
index 3ff6aa602a93e75d31d613d5cd3bade6f7bd8bc0..e8b460b1a85ca2a3015e18790fd1d280a96780a6 100644
--- a/theories/caesium/dune
+++ b/theories/caesium/dune
@@ -3,6 +3,4 @@
  (package refinedrust)
  (flags :standard -w -notation-overridden -w -redundant-canonical-projection)
  (synopsis "Caesium language")
- (theories
-   lithium ; removed by make prepare-install-refinedc
- ))
+ (theories lithium stdpp iris RecordUpdate Ltac2))
diff --git a/theories/lithium/dune b/theories/lithium/dune
index 0e8edefce2919ee9d040528f3b06196ecc094155..ecfc8e8cb0e3899392a140cf2584d6cac9c14c86 100644
--- a/theories/lithium/dune
+++ b/theories/lithium/dune
@@ -2,4 +2,5 @@
  (name lithium)
  (package coq-lithium)
  (flags :standard -w -notation-overridden -w -redundant-canonical-projection)
- (synopsis "Lithium"))
+ (synopsis "Lithium")
+ (theories stdpp iris RecordUpdate Ltac2))
diff --git a/theories/rust_typing/automation/dune b/theories/rust_typing/automation/dune
index 2afd4c4b79788d4ba9c625845ab79b7bb829c1dd..7114e6e3c37514c93a1dfe6f467cf21096cc9f1d 100644
--- a/theories/rust_typing/automation/dune
+++ b/theories/rust_typing/automation/dune
@@ -3,4 +3,4 @@
  (package refinedrust)
  (flags -w -notation-overridden -w -redundant-canonical-projection)
  (synopsis "RefinedRust automation components")
- (theories caesium refinedrust lithium))
+ (theories stdpp iris RecordUpdate Ltac2 caesium refinedrust lithium))
diff --git a/theories/rust_typing/dune b/theories/rust_typing/dune
index 0e4b222cd9a92d0a73d212255bc2141a9c01295f..58c0e901291af9b512be1b271f06552b050fb32e 100644
--- a/theories/rust_typing/dune
+++ b/theories/rust_typing/dune
@@ -3,4 +3,4 @@
  (package refinedrust)
  (flags -w -notation-overridden -w -redundant-canonical-projection)
  (synopsis "RefinedRust")
- (theories caesium lithium))
+ (theories stdpp iris RecordUpdate Ltac2 caesium lithium lrust Equations))