diff --git a/.github/workflows/test-pr.yml b/.github/workflows/test-pr.yml
index 11a28b0f..4094172b 100644
--- a/.github/workflows/test-pr.yml
+++ b/.github/workflows/test-pr.yml
@@ -15,6 +15,7 @@ jobs:
         image:
           - 'coqorg/coq:8.16-ocaml-4.14-flambda'
           - 'coqorg/coq:8.17-ocaml-4.14-flambda'
+          - 'coqorg/coq:8.18-ocaml-4.14-flambda'
       fail-fast: false
     steps:
       - uses: actions/checkout@v3
diff --git a/coq-vlsm.opam b/coq-vlsm.opam
index a6825d53..7c8b3add 100644
--- a/coq-vlsm.opam
+++ b/coq-vlsm.opam
@@ -15,9 +15,9 @@ contains a formalization of VLSMs and their theory in the Coq proof assistant.""
 
 build: ["dune" "build" "-p" name "-j" jobs]
 depends: [
-  "dune" {>= "2.5"}
+  "dune" {>= "3.5"}
   "coq" {>= "8.16"}
-  "coq-stdpp" {>= "1.8.0"}
+  "coq-stdpp" {= "1.8.0"}
   "coq-itauto" 
   "coq-equations" 
 ]
diff --git a/dune-project b/dune-project
index 97a36b24..b06e32db 100644
--- a/dune-project
+++ b/dune-project
@@ -1,3 +1,3 @@
-(lang dune 2.5)
-(using coq 0.2)
+(lang dune 3.5)
+(using coq 0.6)
 (name VLSM)
diff --git a/meta.yml b/meta.yml
index 532bfdb7..63033daa 100644
--- a/meta.yml
+++ b/meta.yml
@@ -3,7 +3,7 @@ fullname: VLSM
 shortname: vlsm
 organization: runtimeverification
 community: false
-dune: false
+dune: true
 action: true
 coqdoc: true
 
@@ -52,9 +52,9 @@ supported_coq_versions:
 dependencies:
 - opam:
     name: coq-stdpp
-    version: '{>= "1.8.0"}'
+    version: '{= "1.8.0"}'
   description: |-
-    [Coq-std++](https://gitlab.mpi-sws.org/iris/stdpp/) 1.8.0 or later
+    [Coq-std++](https://gitlab.mpi-sws.org/iris/stdpp/) 1.8.0
 - opam:
     name: coq-itauto
   description: |-
@@ -67,6 +67,7 @@ dependencies:
 tested_coq_opam_versions:
 - version: '8.16-ocaml-4.14-flambda'
 - version: '8.17-ocaml-4.14-flambda'
+- version: '8.18-ocaml-4.14-flambda'
 
 namespace: VLSM
 
diff --git a/theories/VLSM/dune b/theories/VLSM/dune
index f4e15206..1693a068 100644
--- a/theories/VLSM/dune
+++ b/theories/VLSM/dune
@@ -2,6 +2,7 @@
  (name VLSM)
  (package coq-vlsm)
  (synopsis "Core definitions in Coq for VLSMs")
+ (theories stdpp Cdcl Equations)
  (flags :standard 
    -w -future-coercion-class-field
    -w -deprecated-tacopt-without-locality))