diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml
index ce60ecb..be7c3e1 100644
--- a/.github/workflows/docker-action.yml
+++ b/.github/workflows/docker-action.yml
@@ -15,8 +15,10 @@ jobs:
     strategy:
       matrix:
         image:
-          - 'mathcomp/mathcomp-dev:coq-dev'
-          - 'mathcomp/mathcomp:1.15.0-coq-8.16'
+          - 'mathcomp/mathcomp:1.19.0-coq-8.19'
+          - 'mathcomp/mathcomp:1.18.0-coq-8.18'
+          - 'mathcomp/mathcomp:1.17.0-coq-8.17'
+          - 'mathcomp/mathcomp:1.17.0-coq-8.16'
           - 'mathcomp/mathcomp:1.15.0-coq-8.15'
           - 'mathcomp/mathcomp:1.14.0-coq-8.15'
           - 'mathcomp/mathcomp:1.14.0-coq-8.14'
@@ -24,7 +26,7 @@ jobs:
           - 'mathcomp/mathcomp:1.13.0-coq-8.14'
       fail-fast: false
     steps:
-      - uses: actions/checkout@v3
+      - uses: actions/checkout@v4
       - uses: coq-community/docker-coq-action@v1
         with:
           custom_image: ${{ matrix.image }}
diff --git a/README.md b/README.md
index 76d69a8..6d0e8c2 100644
--- a/README.md
+++ b/README.md
@@ -6,8 +6,8 @@ Follow the instructions on https://github.com/coq-community/templates to regener
 
 [![Docker CI][docker-action-shield]][docker-action-link]
 
-[docker-action-shield]: https://github.com/DistributedComponents/disel/workflows/Docker%20CI/badge.svg?branch=master
-[docker-action-link]: https://github.com/DistributedComponents/disel/actions?query=workflow:"Docker%20CI"
+[docker-action-shield]: https://github.com/DistributedComponents/disel/actions/workflows/docker-action.yml/badge.svg?branch=master
+[docker-action-link]: https://github.com/DistributedComponents/disel/actions/workflows/docker-action.yml
 
 
 
@@ -28,7 +28,7 @@ from implementation details.
 - License: [BSD 2-Clause "Simplified" license](LICENSE)
 - Compatible Coq versions: 8.14 or later
 - Additional dependencies:
-  - [MathComp](https://math-comp.github.io) 1.13.0 or later (`ssreflect` suffices)
+  - [MathComp](https://math-comp.github.io) 1.13.0 to 1.19.0 (`ssreflect` suffices)
   - [FCSL PCM](https://github.com/imdea-software/fcsl-pcm) 1.7.0 or later
   - [Hoare Type Theory](https://github.com/imdea-software/htt) 1.2.0 or later
 - Coq namespace: `DiSeL`
diff --git a/coq-disel-calculator.opam b/coq-disel-calculator.opam
index 16c26e3..9de9e00 100644
--- a/coq-disel-calculator.opam
+++ b/coq-disel-calculator.opam
@@ -12,7 +12,7 @@ build: [make "-j%{jobs}%" "calculator"]
 depends: [
   "ocaml" {>= "4.05.0"}
   "coq" {>= "8.14"}
-  "coq-mathcomp-ssreflect" {>= "1.13"}
+  "coq-mathcomp-ssreflect" {>= "1.13" & < "2.0"}
   "coq-fcsl-pcm" {>= "1.7.0"}
   "coq-htt" {>= "1.2.0"}
   "ocamlbuild" {build}
diff --git a/coq-disel-examples.opam b/coq-disel-examples.opam
index 72a97f4..1c49e6e 100644
--- a/coq-disel-examples.opam
+++ b/coq-disel-examples.opam
@@ -10,9 +10,9 @@ synopsis: "Example systems for Disel, a separation-style logic for compositional
 
 build: ["dune" "build" "-p" name "-j" jobs]
 depends: [
-  "dune" {>= "2.5"}
+  "dune" {>= "3.5"}
   "coq" {>= "8.14"}
-  "coq-mathcomp-ssreflect" {>= "1.13"}
+  "coq-mathcomp-ssreflect" {>= "1.13" & < "2.0"}
   "coq-fcsl-pcm" {>= "1.7.0"}
   "coq-disel" {= version}
 ]
diff --git a/coq-disel-tpc.opam b/coq-disel-tpc.opam
index bb99ac2..7257a46 100644
--- a/coq-disel-tpc.opam
+++ b/coq-disel-tpc.opam
@@ -12,7 +12,7 @@ build: [make "-j%{jobs}%" "tpc"]
 depends: [
   "ocaml" {>= "4.05.0"}
   "coq" {>= "8.14"}
-  "coq-mathcomp-ssreflect" {>= "1.13"}
+  "coq-mathcomp-ssreflect" {>= "1.13" & < "2.0"}
   "coq-fcsl-pcm" {>= "1.7.0"}
   "coq-htt" {>= "1.2.0"}
   "ocamlbuild" {build}
diff --git a/coq-disel.opam b/coq-disel.opam
index 1e68177..595ddce 100644
--- a/coq-disel.opam
+++ b/coq-disel.opam
@@ -19,9 +19,9 @@ from implementation details."""
 
 build: ["dune" "build" "-p" name "-j" jobs]
 depends: [
-  "dune" {>= "2.5"}
+  "dune" {>= "3.5"}
   "coq" {>= "8.14"}
-  "coq-mathcomp-ssreflect" {>= "1.13"}
+  "coq-mathcomp-ssreflect" {>= "1.13" & < "2.0"}
   "coq-fcsl-pcm" {>= "1.7.0"}
   "coq-htt" {>= "1.2.0"}
 ]
diff --git a/dune-project b/dune-project
index 7e6db9a..9e538be 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 disel)
diff --git a/meta.yml b/meta.yml
index 413be38..f7d90c2 100644
--- a/meta.yml
+++ b/meta.yml
@@ -46,9 +46,13 @@ supported_coq_versions:
   opam: '{>= "8.14"}'
 
 tested_coq_opam_versions:
-- version: 'coq-dev'
-  repo: 'mathcomp/mathcomp-dev'
-- version: '1.15.0-coq-8.16'
+- version: '1.19.0-coq-8.19'
+  repo: 'mathcomp/mathcomp'
+- version: '1.18.0-coq-8.18'
+  repo: 'mathcomp/mathcomp'
+- version: '1.17.0-coq-8.17'
+  repo: 'mathcomp/mathcomp'
+- version: '1.17.0-coq-8.16'
   repo: 'mathcomp/mathcomp'
 - version: '1.15.0-coq-8.15'
   repo: 'mathcomp/mathcomp'
@@ -64,9 +68,9 @@ tested_coq_opam_versions:
 dependencies:
 - opam:
     name: coq-mathcomp-ssreflect
-    version: '{>= "1.13"}'
+    version: '{>= "1.13" & < "2.0"}'
   description: |-
-    [MathComp](https://math-comp.github.io) 1.13.0 or later (`ssreflect` suffices)
+    [MathComp](https://math-comp.github.io) 1.13.0 to 1.19.0 (`ssreflect` suffices)
 - opam:
     name: coq-fcsl-pcm
     version: '{>= "1.7.0"}'