diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 83d25c869d2b9770e1e7fd55bdac616887187064..4e296ed41c5e626aa6e3f8b9d618611fea8f167d 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -29,7 +29,7 @@ stages:
     - opam install -y -v -j ${NJOBS} coq-prosa-refinements
 
 .preferred-stable-version:
-    image: bbbrandenburg/mathcomp-for-prosa:1.17.0-coq-8.18
+    image: bbbrandenburg/mathcomp-for-prosa:1.18.0-coq-8.18
 
 .build:
   image: bbbrandenburg/mathcomp-for-prosa:${CI_JOB_NAME}
@@ -81,6 +81,11 @@ stages:
     - .build
     - .not_in_wip_branches
 
+1.18.0-coq-8.18:
+  extends:
+    - .build
+    - .not_in_wip_branches
+
 POET:
   extends:
     - .build-and-test-POET
@@ -174,7 +179,7 @@ proof-state:
   extends:
    - .not_in_wip_branches
   stage: build
-  image: bbbrandenburg/alectryon-ci:1.17.0-coq-8.18
+  image: bbbrandenburg/alectryon-ci:1.18.0-coq-8.18
   script:
     - eval $(opam env)
     - make -j ${NJOBS} all
diff --git a/coq-prosa.opam b/coq-prosa.opam
index 9a5938c4967cfae5227e8dae6e5109f4f467b47d..70038fe81970b14fccdb6078c416da6f3d633111 100644
--- a/coq-prosa.opam
+++ b/coq-prosa.opam
@@ -13,7 +13,7 @@ build: [
 install: [make "install"]
 depends: [
   "coq" {((>= "8.16" & < "8.19~") | = "dev")}
-  "coq-mathcomp-algebra" {((>= "1.16" & < "1.18~") | = "dev")}
+  "coq-mathcomp-algebra" {((>= "1.16" & < "1.19~") | = "dev")}
   "coq-mathcomp-zify" {>= "1.2.0"}
 ]