From 1e50c6accda8da5d5a0b2c0423d035b6f6f6f6a6 Mon Sep 17 00:00:00 2001
From: Reynald Affeldt <reynald.affeldt@aist.go.jp>
Date: Thu, 13 Jun 2024 20:54:24 +0900
Subject: [PATCH] CI

---
 .github/workflows/docker-action.yml | 1 -
 README.md                           | 2 +-
 coq-infotheo.opam                   | 2 +-
 meta.yml                            | 6 ++----
 4 files changed, 4 insertions(+), 7 deletions(-)

diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml
index 0e80a934..edc24fd9 100644
--- a/.github/workflows/docker-action.yml
+++ b/.github/workflows/docker-action.yml
@@ -17,7 +17,6 @@ jobs:
     strategy:
       matrix:
         image:
-          - 'mathcomp/mathcomp:2.2.0-coq-8.17'
           - 'mathcomp/mathcomp:2.2.0-coq-8.18'
           - 'mathcomp/mathcomp:2.2.0-coq-8.19'
       fail-fast: false
diff --git a/README.md b/README.md
index 11d24c75..a97dc1cf 100644
--- a/README.md
+++ b/README.md
@@ -32,7 +32,7 @@ information theory, and linear error-correcting codes.
   - Naruomi Obata, Titech (M2)
   - Alessandro Bruni, IT-University of Copenhagen
 - License: [LGPL-2.1-or-later](LICENSE)
-- Compatible Coq versions: Coq 8.17--8.19
+- Compatible Coq versions: Coq 8.18--8.19
 - Additional dependencies:
   - [MathComp ssreflect](https://math-comp.github.io)
   - [MathComp fingroup](https://math-comp.github.io)
diff --git a/coq-infotheo.opam b/coq-infotheo.opam
index 40f28435..97f0969e 100644
--- a/coq-infotheo.opam
+++ b/coq-infotheo.opam
@@ -21,7 +21,7 @@ build: [
 ]
 install: [make "install"]
 depends: [
-  "coq" { (>= "8.17" & < "8.20~") | (= "dev") }
+  "coq" { (>= "8.18" & < "8.20~") | (= "dev") }
   "coq-mathcomp-ssreflect" { (>= "2.2.0") | (= "dev") }
   "coq-mathcomp-fingroup" { (>= "2.2.0") | (= "dev")  }
   "coq-mathcomp-algebra" { (>= "2.2.0") | (= "dev")  }
diff --git a/meta.yml b/meta.yml
index 7dbbb61a..9eb8a2dc 100644
--- a/meta.yml
+++ b/meta.yml
@@ -43,12 +43,10 @@ license:
 nix: true
 
 supported_coq_versions:
-  text: Coq 8.17--8.19
-  opam: '{ (>= "8.17" & < "8.20~") | (= "dev") }'
+  text: Coq 8.18--8.19
+  opam: '{ (>= "8.18" & < "8.20~") | (= "dev") }'
 
 tested_coq_opam_versions:
-- version: '2.2.0-coq-8.17'
-  repo: 'mathcomp/mathcomp'
 - version: '2.2.0-coq-8.18'
   repo: 'mathcomp/mathcomp'
 - version: '2.2.0-coq-8.19'