From 53845b0ec7608c5a95c936d60d85e957f3e32201 Mon Sep 17 00:00:00 2001
From: Takafumi Saikawa <tscompor@gmail.com>
Date: Fri, 19 Dec 2025 22:48:35 +0900
Subject: [PATCH] require mathcomp 2.5.0

---
 .github/workflows/docker-action.yml |  1 -
 coq-monae.opam                      | 10 +++++-----
 2 files changed, 5 insertions(+), 6 deletions(-)

diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml
index 219c7549..3c319e4e 100644
--- a/.github/workflows/docker-action.yml
+++ b/.github/workflows/docker-action.yml
@@ -17,7 +17,6 @@ jobs:
     strategy:
       matrix:
         image:
-          - 'mathcomp/mathcomp:2.4.0-rocq-prover-9.0'
           - 'mathcomp/mathcomp:2.5.0-rocq-prover-9.0'
       fail-fast: false
     steps:
diff --git a/coq-monae.opam b/coq-monae.opam
index 39da201e..b30874b5 100644
--- a/coq-monae.opam
+++ b/coq-monae.opam
@@ -19,11 +19,11 @@ build: [make "-j%{jobs}%"]
 install: [make "install_full"]
 depends: [
   "coq" { (>= "9.0" & < "9.1~") }
-  "coq-mathcomp-ssreflect" { (>= "2.4.0") }
-  "coq-mathcomp-fingroup" { (>= "2.4.0") }
-  "coq-mathcomp-algebra" { (>= "2.4.0") }
-  "coq-mathcomp-solvable" { (>= "2.4.0") }
-  "coq-mathcomp-field" { (>= "2.4.0") }
+  "coq-mathcomp-ssreflect" { (>= "2.5.0") }
+  "coq-mathcomp-fingroup" { (>= "2.5.0") }
+  "coq-mathcomp-algebra" { (>= "2.5.0") }
+  "coq-mathcomp-solvable" { (>= "2.5.0") }
+  "coq-mathcomp-field" { (>= "2.5.0") }
   "coq-mathcomp-analysis" { (>= "1.12.0")}
   "coq-infotheo" { >= "0.9.5"}
   "coq-paramcoq" { >= "1.1.3" & < "1.2~" }