diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml
index 23287ab..2aaf380 100644
--- a/.github/workflows/docker-action.yml
+++ b/.github/workflows/docker-action.yml
@@ -19,6 +19,7 @@ jobs:
         image:
           - 'mathcomp/mathcomp:2.2.0-coq-8.19'
           - 'mathcomp/mathcomp:2.3.0-coq-8.20'
+          - 'mathcomp/mathcomp:2.4.0-rocq-prover-9.0'
           - 'mathcomp/mathcomp-dev:rocq-prover-dev'
       fail-fast: false
     steps:
diff --git a/README.md b/README.md
index 5e92ee4..1099810 100644
--- a/README.md
+++ b/README.md
@@ -41,7 +41,8 @@ that HTT implements Separation logic as a shallow embedding in Coq.
 - License: [Apache-2.0](LICENSE)
 - Compatible Coq versions: 8.19 or later
 - Additional dependencies:
-  - [MathComp ssreflect 2.2-2.3](https://math-comp.github.io)
+  - [Hierarchy Builder 1.7.0 or later](https://github.com/math-comp/hierarchy-builder)
+  - [MathComp ssreflect 2.2 or later](https://math-comp.github.io)
   - [MathComp algebra](https://math-comp.github.io)
   - [MathComp fingroup](https://math-comp.github.io)
   - [FCSL-PCM 2.1](https://github.com/imdea-software/fcsl-pcm)
diff --git a/coq-htt-core.opam b/coq-htt-core.opam
index b856b31..2d78443 100644
--- a/coq-htt-core.opam
+++ b/coq-htt-core.opam
@@ -31,11 +31,11 @@ variables). The connection reconciles dependent types with effects of state and
 establishes Separation logic as a type theory for such effects. In implementation terms, it means
 that HTT implements Separation logic as a shallow embedding in Coq."""
 
-build: [make "-C" "htt" "-j%{jobs}%"]
-install: [make "-C" "htt" "install"]
+build: ["dune" "build" "-p" name "-j" jobs]
 depends: [
   "dune" {>= "3.6"}
   "coq" { (>= "8.19" & < "9.1~") | (= "dev") }
+  "coq-hierarchy-builder" { (>= "1.7.0" & < "1.10~") | (= "dev") }
   "coq-mathcomp-ssreflect" { (>= "2.2.0" & < "2.5~") | (= "dev") }
   "coq-mathcomp-algebra" 
   "coq-mathcomp-fingroup" 
diff --git a/meta.yml b/meta.yml
index 74003c1..da7bebe 100644
--- a/meta.yml
+++ b/meta.yml
@@ -88,15 +88,23 @@ tested_coq_opam_versions:
   repo: 'mathcomp/mathcomp'
 - version: '2.3.0-coq-8.20'
   repo: 'mathcomp/mathcomp'
+- version: '2.4.0-rocq-prover-9.0'
+  repo: 'mathcomp/mathcomp'
 - version: 'rocq-prover-dev'
   repo: 'mathcomp/mathcomp-dev'
 
+
 dependencies:
+- opam:
+    name: coq-hierarchy-builder
+    version: '{ (>= "1.7.0" & < "1.10~") | (= "dev") }'
+  description: |-
+    [Hierarchy Builder 1.7.0 or later](https://github.com/math-comp/hierarchy-builder)
 - opam:
     name: coq-mathcomp-ssreflect
-    version: '{ (>= "2.2.0" & < "2.4~") | (= "dev") }'
+    version: '{ (>= "2.2.0" & < "2.5~") | (= "dev") }'
   description: |-
-    [MathComp ssreflect 2.2-2.3](https://math-comp.github.io)
+    [MathComp ssreflect 2.2 or later](https://math-comp.github.io)
 - opam:
     name: coq-mathcomp-algebra
   description: |-