diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml
index 0ba560f..23287ab 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:
@@ -17,37 +19,15 @@ jobs:
         image:
           - 'mathcomp/mathcomp:2.2.0-coq-8.19'
           - 'mathcomp/mathcomp:2.3.0-coq-8.20'
-          - 'mathcomp/mathcomp-dev:coq-dev'
+          - 'mathcomp/mathcomp-dev:rocq-prover-dev'
       fail-fast: false
     steps:
       - 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 e0c132c..5e92ee4 100644
--- a/README.md
+++ b/README.md
@@ -39,7 +39,7 @@ that HTT implements Separation logic as a shallow embedding in Coq.
   - Alexander Gryzlov
   - Marcos Grandury
 - License: [Apache-2.0](LICENSE)
-- Compatible Coq versions: Coq 8.19 to 8.20
+- Compatible Coq versions: 8.19 or later
 - Additional dependencies:
   - [MathComp ssreflect 2.2-2.3](https://math-comp.github.io)
   - [MathComp algebra](https://math-comp.github.io)
diff --git a/coq-htt-core.opam b/coq-htt-core.opam
index e342fd1..8182418 100644
--- a/coq-htt-core.opam
+++ b/coq-htt-core.opam
@@ -35,7 +35,7 @@ build: [make "-C" "htt" "-j%{jobs}%"]
 install: [make "-C" "htt" "install"]
 depends: [
   "dune" {>= "3.6"}
-  "coq" { (>= "8.19" & < "8.21~") | (= "dev") }
+  "coq" { (>= "8.19" & < "9.1~") | (= "dev") }
   "coq-mathcomp-ssreflect" { (>= "2.2.0" & < "2.4~") | (= "dev") }
   "coq-mathcomp-algebra" 
   "coq-mathcomp-fingroup" 
diff --git a/meta.yml b/meta.yml
index 7c13da7..74003c1 100644
--- a/meta.yml
+++ b/meta.yml
@@ -80,15 +80,15 @@ license:
   file: LICENSE
 
 supported_coq_versions:
-  text: Coq 8.19 to 8.20
-  opam: '{ (>= "8.19" & < "8.21~") | (= "dev") }'
+  text: 8.19 or later
+  opam: '{ (>= "8.19" & < "9.1~") | (= "dev") }'
 
 tested_coq_opam_versions:
 - version: '2.2.0-coq-8.19'
   repo: 'mathcomp/mathcomp'
 - version: '2.3.0-coq-8.20'
   repo: 'mathcomp/mathcomp'
-- version: 'coq-dev'
+- version: 'rocq-prover-dev'
   repo: 'mathcomp/mathcomp-dev'
 
 dependencies:
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"))