diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml
index c8a1815..4705a8c 100644
--- a/.github/workflows/docker-action.yml
+++ b/.github/workflows/docker-action.yml
@@ -19,19 +19,21 @@ jobs:
     strategy:
       matrix:
         image:
-          - 'mathcomp/mathcomp-dev:coq-dev'
-          - 'mathcomp/mathcomp:1.14.0-coq-8.15'
-          - 'mathcomp/mathcomp:1.13.0-coq-8.14'
-          - 'mathcomp/mathcomp:1.12.0-coq-8.13'
-          - 'mathcomp/mathcomp:1.11.0-coq-8.12'
+          - 'mathcomp/mathcomp:2.2.0-coq-8.17'
+          - 'mathcomp/mathcomp:2.2.0-coq-8.16'
+          - 'mathcomp/mathcomp:2.1.0-coq-8.17'
+          - 'mathcomp/mathcomp:2.1.0-coq-8.16'
+          - 'mathcomp/mathcomp:2.0.0-coq-8.17'
+          - 'mathcomp/mathcomp:2.0.0-coq-8.16'
       fail-fast: false
     steps:
-      - uses: actions/checkout@v2
+      - uses: actions/checkout@v3
       - uses: coq-community/docker-coq-action@v1
         with:
           opam_file: 'coq-comp-dec-modal.opam'
           custom_image: ${{ matrix.image }}
 
+
 # See also:
 # https://github.com/coq-community/docker-coq-action#readme
 # https://github.com/erikmd/docker-coq-github-action-demo
diff --git a/README.md b/README.md
index 542796e..a5e8964 100644
--- a/README.md
+++ b/README.md
@@ -11,8 +11,8 @@ Follow the instructions on https://github.com/coq-community/templates to regener
 [![coqdoc][coqdoc-shield]][coqdoc-link]
 [![DOI][doi-shield]][doi-link]
 
-[docker-action-shield]: https://github.com/coq-community/comp-dec-modal/workflows/Docker%20CI/badge.svg?branch=master
-[docker-action-link]: https://github.com/coq-community/comp-dec-modal/actions?query=workflow:"Docker%20CI"
+[docker-action-shield]: https://github.com/coq-community/comp-dec-modal/actions/workflows/docker-action.yml/badge.svg?branch=master
+[docker-action-link]: https://github.com/coq-community/comp-dec-modal/actions/workflows/docker-action.yml
 
 [contributing-shield]: https://img.shields.io/badge/contributions-welcome-%23f7931e.svg
 [contributing-link]: https://github.com/coq-community/manifesto/blob/master/CONTRIBUTING.md
@@ -52,9 +52,10 @@ of said algorithm.
 - Coq-community maintainer(s):
   - Christian Doczkal ([**@chdoc**](https://github.com/chdoc))
 - License: [CeCILL-B](LICENSE)
-- Compatible Coq versions: 8.12 or later
+- Compatible Coq versions: 8.16 and 8.17
 - Additional dependencies:
-  - [MathComp](https://math-comp.github.io) 1.11.0 or later (`ssreflect` suffices)
+  - [MathComp](https://math-comp.github.io) 2.0 or later (`ssreflect` suffices)
+  - [Hierarchy Builder](https://github.com/math-comp/hierarchy-builder) 1.6.0 or later
 - Coq namespace: `CompDecModal`
 - Related publication(s):
   - [A Machine-Checked Constructive Metatheory of Computation Tree Logic](https://www.ps.uni-saarland.de/static/doczkal-diss/index.php) doi:[10.22028/D291-26649](https://doi.org/10.22028/D291-26649)
diff --git a/coq-comp-dec-modal.opam b/coq-comp-dec-modal.opam
index 6a0a4fc..2a0b8d9 100644
--- a/coq-comp-dec-modal.opam
+++ b/coq-comp-dec-modal.opam
@@ -32,8 +32,9 @@ of said algorithm.
 build: [make "-j%{jobs}%"]
 install: [make "install"]
 depends: [
-  "coq" {(>= "8.12" & < "8.16~") | (= "dev")}
-  "coq-mathcomp-ssreflect" {(>= "1.11" & < "1.15~") | (= "dev")}
+  "coq" {>= "8.16" & < "8.18"}
+  "coq-mathcomp-ssreflect" {>= "2.0"}
+  "coq-hierarchy-builder" {>= "1.6.0"}
 ]
 
 tags: [
diff --git a/meta.yml b/meta.yml
index c66be64..07ed94b 100644
--- a/meta.yml
+++ b/meta.yml
@@ -52,31 +52,37 @@ license:
   identifier: CECILL-B
 
 supported_coq_versions:
-  text: 8.12 or later
-  opam: '{(>= "8.12" & < "8.16~") | (= "dev")}'
+  text: 8.16 and 8.17
+  opam: '{>= "8.16" & < "8.18"}'
 
 tested_coq_opam_versions:
-- version: 'coq-dev'
-  repo: 'mathcomp/mathcomp-dev'
-- version: '1.14.0-coq-8.15'
+- version: '2.2.0-coq-8.17'
   repo: 'mathcomp/mathcomp'
-- version: '1.13.0-coq-8.14'
+- version: '2.2.0-coq-8.16'
   repo: 'mathcomp/mathcomp'
-- version: '1.12.0-coq-8.13'
+- version: '2.1.0-coq-8.17'
   repo: 'mathcomp/mathcomp'
-- version: '1.11.0-coq-8.12'
+- version: '2.1.0-coq-8.16'
+  repo: 'mathcomp/mathcomp'
+- version: '2.0.0-coq-8.17'
+  repo: 'mathcomp/mathcomp'
+- version: '2.0.0-coq-8.16'
   repo: 'mathcomp/mathcomp'
 
 # “At 01:42 on Sunday.”
 ci_cron_schedule: '42 1 * * 0'
-    
+
 dependencies:
 - opam:
     name: coq-mathcomp-ssreflect
-    version: '{(>= "1.11" & < "1.15~") | (= "dev")}'
-  nix: ssreflect
+    version: '{>= "2.0"}'
+  description: |-
+    [MathComp](https://math-comp.github.io) 2.0 or later (`ssreflect` suffices)
+- opam:
+    name: coq-hierarchy-builder
+    version: '{>= "1.6.0"}'
   description: |-
-    [MathComp](https://math-comp.github.io) 1.11.0 or later (`ssreflect` suffices)
+    [Hierarchy Builder](https://github.com/math-comp/hierarchy-builder) 1.6.0 or later
 
 namespace: CompDecModal