CI

affeldt-aist · Jun 13, 2024 · 1e50c6a · 1e50c6a
1 parent 5f063a7
commit 1e50c6a
Show file tree

Hide file tree

Showing 4 changed files with 4 additions and 7 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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'