diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml
index 6a7c9c8..a774d92 100644
--- a/.github/workflows/docker-action.yml
+++ b/.github/workflows/docker-action.yml
@@ -17,7 +17,7 @@ jobs:
       matrix:
         image:
           - 'mathcomp/mathcomp:1.17.0-coq-8.15'
-          - 'mathcomp/mathcomp:1.17.0-coq-8.17'
+          - 'mathcomp/mathcomp:1.17.0-coq-8.18'
       fail-fast: false
     steps:
       - uses: actions/checkout@v2
diff --git a/README.md b/README.md
index 69e2e11..0fe5f74 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/imdea-software/htt/workflows/Docker%20CI/badge.svg?branch=master
-[docker-action-link]: https://github.com/imdea-software/htt/actions?query=workflow:"Docker%20CI"
+[docker-action-shield]: https://github.com/imdea-software/htt/actions/workflows/docker-action.yml/badge.svg?branch=master
+[docker-action-link]: https://github.com/imdea-software/htt/actions/workflows/docker-action.yml
 
 
 
diff --git a/coq-htt-examples.opam b/coq-htt-examples.opam
index 138b09a..caeded0 100644
--- a/coq-htt-examples.opam
+++ b/coq-htt-examples.opam
@@ -33,7 +33,7 @@ that HTT implements Separation logic as a shallow embedding in Coq."""
 build: [make "-j%{jobs}%"]
 install: [make "install"]
 depends: [
-  "coq" { (>= "8.15" & < "8.18~") | (= "dev") }
+  "coq" { (>= "8.15" & < "8.19~") | (= "dev") }
   "coq-mathcomp-ssreflect" { (>= "1.17.0" & < "1.18~") | (= "dev") }
   "coq-mathcomp-algebra" 
   "coq-mathcomp-fingroup" 
diff --git a/coq-htt.opam b/coq-htt.opam
index c817cad..1517652 100644
--- a/coq-htt.opam
+++ b/coq-htt.opam
@@ -34,7 +34,7 @@ that HTT implements Separation logic as a shallow embedding in Coq."""
 build: ["dune" "build" "-p" name "-j" jobs]
 depends: [
   "dune" {>= "2.5"}
-  "coq" { (>= "8.15" & < "8.18~") | (= "dev") }
+  "coq" { (>= "8.15" & < "8.19~") | (= "dev") }
   "coq-mathcomp-ssreflect" { (>= "1.17.0" & < "1.18~") | (= "dev") }
   "coq-mathcomp-algebra" 
   "coq-mathcomp-fingroup" 
diff --git a/meta.yml b/meta.yml
index a693f83..3944bf1 100644
--- a/meta.yml
+++ b/meta.yml
@@ -79,12 +79,12 @@ license:
 
 supported_coq_versions:
   text: Coq 8.15 to 8.17
-  opam: '{ (>= "8.15" & < "8.18~") | (= "dev") }'
+  opam: '{ (>= "8.15" & < "8.19~") | (= "dev") }'
 
 tested_coq_opam_versions:
 - version: '1.17.0-coq-8.15'
   repo: 'mathcomp/mathcomp'
-- version: '1.17.0-coq-8.17'
+- version: '1.17.0-coq-8.18'
   repo: 'mathcomp/mathcomp'
 # - version: 'coq-dev'
 #  repo: 'mathcomp/mathcomp-dev'