update dune version

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"}
 ]
 

dune-project

-(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)

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))

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))

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))

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))

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))