diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml
index fea2e087..fba646be 100644
--- a/.github/workflows/docker-action.yml
+++ b/.github/workflows/docker-action.yml
@@ -19,8 +19,10 @@ jobs:
         image:
           - 'mathcomp/mathcomp:1.17.0-coq-8.17'
           - 'mathcomp/mathcomp:1.18.0-coq-8.17'
+          - 'mathcomp/mathcomp:1.19.0-coq-8.17'
           - 'mathcomp/mathcomp:1.17.0-coq-8.18'
           - 'mathcomp/mathcomp:1.18.0-coq-8.18'
+          - 'mathcomp/mathcomp:1.19.0-coq-8.18'
       fail-fast: false
     steps:
       - uses: actions/checkout@v2
diff --git a/coq-infotheo.opam b/coq-infotheo.opam
index ec3ca2a2..08ab81ac 100644
--- a/coq-infotheo.opam
+++ b/coq-infotheo.opam
@@ -22,12 +22,12 @@ build: [
 install: [make "install"]
 depends: [
   "coq" { (>= "8.17" & < "8.19~") | (= "dev") }
-  "coq-mathcomp-ssreflect" { (>= "1.16.0" & < "1.19~") | (= "dev") }
-  "coq-mathcomp-fingroup" { (>= "1.16.0" & < "1.19~") | (= "dev")  }
-  "coq-mathcomp-algebra" { (>= "1.16.0" & < "1.19~") | (= "dev")  }
-  "coq-mathcomp-solvable" { (>= "1.16.0" & < "1.19~") | (= "dev")  }
-  "coq-mathcomp-field" { (>= "1.16.0" & < "1.19~") | (= "dev")  }
-  "coq-mathcomp-analysis" { (>= "0.6.6") & (< "0.7~")}
+  "coq-mathcomp-ssreflect" { (>= "1.16.0" & < "1.20.0") | (= "dev") }
+  "coq-mathcomp-fingroup" { (>= "1.16.0" & < "1.20.0") | (= "dev")  }
+  "coq-mathcomp-algebra" { (>= "1.16.0" & < "1.20.0") | (= "dev")  }
+  "coq-mathcomp-solvable" { (>= "1.16.0" & < "1.20.0") | (= "dev")  }
+  "coq-mathcomp-field" { (>= "1.16.0" & < "1.20.0") | (= "dev")  }
+  "coq-mathcomp-analysis" { (>= "0.6.6") & (< "0.8~")}
   "coq-hierarchy-builder" { = "1.5.0" }
   "coq-mathcomp-algebra-tactics" { = "1.1.1" }
 ]
diff --git a/meta.yml b/meta.yml
index 6376f69c..5edabcfa 100644
--- a/meta.yml
+++ b/meta.yml
@@ -49,40 +49,44 @@ tested_coq_opam_versions:
   repo: 'mathcomp/mathcomp'
 - version: '1.18.0-coq-8.17'
   repo: 'mathcomp/mathcomp'
+- version: '1.19.0-coq-8.17'
+  repo: 'mathcomp/mathcomp'
 - version: '1.17.0-coq-8.18'
   repo: 'mathcomp/mathcomp'
 - version: '1.18.0-coq-8.18'
   repo: 'mathcomp/mathcomp'
+- version: '1.19.0-coq-8.18'
+  repo: 'mathcomp/mathcomp'
 
 dependencies:
 - opam:
     name: coq-mathcomp-ssreflect
-    version: '{ (>= "1.16.0" & < "1.19~") | (= "dev") }'
+    version: '{ (>= "1.16.0" & < "1.20.0") | (= "dev") }'
   description: |-
     [MathComp ssreflect](https://math-comp.github.io)
 - opam:
     name: coq-mathcomp-fingroup
-    version: '{ (>= "1.16.0" & < "1.19~") | (= "dev")  }'
+    version: '{ (>= "1.16.0" & < "1.20.0") | (= "dev")  }'
   description: |-
     [MathComp fingroup](https://math-comp.github.io)
 - opam:
     name: coq-mathcomp-algebra
-    version: '{ (>= "1.16.0" & < "1.19~") | (= "dev")  }'
+    version: '{ (>= "1.16.0" & < "1.20.0") | (= "dev")  }'
   description: |-
     [MathComp algebra](https://math-comp.github.io)
 - opam:
     name: coq-mathcomp-solvable
-    version: '{ (>= "1.16.0" & < "1.19~") | (= "dev")  }'
+    version: '{ (>= "1.16.0" & < "1.20.0") | (= "dev")  }'
   description: |-
     [MathComp solvable](https://math-comp.github.io)
 - opam:
     name: coq-mathcomp-field
-    version: '{ (>= "1.16.0" & < "1.19~") | (= "dev")  }'
+    version: '{ (>= "1.16.0" & < "1.20.0") | (= "dev")  }'
   description: |-
     [MathComp field](https://math-comp.github.io)
 - opam:
     name: coq-mathcomp-analysis
-    version: '{ (>= "0.6.6") & (< "0.7~")}'
+    version: '{ (>= "0.6.6") & (< "0.8~")}'
   description: |-
     [MathComp analysis](https://github.com/math-comp/analysis)
 - opam: