diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml
index e02d2c0..6bacde4 100644
--- a/.github/workflows/docker-action.yml
+++ b/.github/workflows/docker-action.yml
@@ -1,3 +1,5 @@
+# This file was generated from `meta.yml`, please do not edit manually.
+# Follow the instructions on https://github.com/coq-community/templates to regenerate.
 name: Docker CI
 
 on:
@@ -23,31 +25,9 @@ jobs:
       - uses: actions/checkout@v4
       - uses: coq-community/docker-coq-action@v1
         with:
+          opam_file: 'coq-htt-core.opam'
           custom_image: ${{ matrix.image }}
-          custom_script: |
-            {{before_install}}
-            startGroup "Build htt-core dependencies"
-              opam pin add -n -y -k path coq-htt-core .
-              opam update -y
-              opam install -y -j $(nproc) coq-htt-core --deps-only
-            endGroup
-            startGroup "Build htt-core"
-              opam install -y -v -j $(nproc) coq-htt-core
-              opam list
-            endGroup
-            startGroup "Build htt dependencies"
-              opam pin add -n -y -k path coq-htt .
-              opam update -y
-              opam install -y -j $(nproc) coq-htt --deps-only
-            endGroup
-            startGroup "Build coq-htt"
-              opam install -y -v -j $(nproc) coq-htt
-              opam list
-            endGroup
-            startGroup "Uninstallation test"
-              opam remove -y coq-htt
-              opam remove -y coq-htt-core
-            endGroup
+
 
 # See also:
 # https://github.com/coq-community/docker-coq-action#readme
diff --git a/README.md b/README.md
index 8213b20..9ffb03c 100644
--- a/README.md
+++ b/README.md
@@ -45,7 +45,7 @@ that HTT implements Separation logic as a shallow embedding in Coq.
   - [MathComp algebra](https://math-comp.github.io)
   - [MathComp fingroup](https://math-comp.github.io)
   - [FCSL-PCM 2.0](https://github.com/imdea-software/fcsl-pcm)
-  - [Dune](https://dune.build) 2.5 or later
+  - [Dune](https://dune.build) 3.6 or later
 - Coq namespace: `htt`
 - Related publication(s):
   - [Structuring the verification of heap-manipulating programs](https://software.imdea.org/~aleks/papers/reflect/reflect.pdf) doi:[10.1145/1706299.1706331](https://doi.org/10.1145/1706299.1706331)
diff --git a/coq-htt-core.opam b/coq-htt-core.opam
index 1a20705..74837d7 100644
--- a/coq-htt-core.opam
+++ b/coq-htt-core.opam
@@ -3,7 +3,7 @@
 
 opam-version: "2.0"
 maintainer: "fcsl@software.imdea.org"
-version: "dev"
+version: "2.0.1"
 
 homepage: "https://github.com/imdea-software/htt"
 dev-repo: "git+https://github.com/imdea-software/htt.git"
@@ -35,7 +35,7 @@ build: ["dune" "build" "-p" name "-j" jobs]
 depends: [
   "dune" {>= "3.6"}
   "coq" { (>= "8.19" & < "8.21~") | (= "dev") }
-  "coq-mathcomp-ssreflect" { (>= "2.2.0" & < "2.3~") | (= "dev") }
+  "coq-mathcomp-ssreflect" { (>= "2.2.0" & < "2.4~") | (= "dev") }
   "coq-mathcomp-algebra" 
   "coq-mathcomp-fingroup" 
   "coq-fcsl-pcm" { (>= "2.0.0" & < "2.1~") | (= "dev") }
diff --git a/meta.yml b/meta.yml
index b8388ff..299e408 100644
--- a/meta.yml
+++ b/meta.yml
@@ -72,7 +72,7 @@ maintainers:
 
 opam-file-maintainer: fcsl@software.imdea.org
 
-opam-file-version: dev
+opam-file-version: 2.0.1
 
 license:
   fullname: Apache-2.0
@@ -94,7 +94,7 @@ tested_coq_opam_versions:
 dependencies:
 - opam:
     name: coq-mathcomp-ssreflect
-    version: '{ (>= "2.2.0" & < "2.3~") | (= "dev") }'
+    version: '{ (>= "2.2.0" & < "2.4~") | (= "dev") }'
   description: |-
     [MathComp ssreflect 2.2](https://math-comp.github.io)
 - opam:
diff --git a/theories/dune b/theories/dune
new file mode 100644
index 0000000..8f51667
--- /dev/null
+++ b/theories/dune
@@ -0,0 +1,7 @@
+; This file was generated from `meta.yml`, please do not edit manually.
+; Follow the instructions on https://github.com/coq-community/templates to regenerate.
+
+(coq.theory
+ (name htt)
+ (package coq-htt-core)
+ (synopsis "Hoare Type Theory"))