diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml index 4fc5566..c7429ea 100644 --- a/.github/workflows/docker-action.yml +++ b/.github/workflows/docker-action.yml @@ -17,13 +17,13 @@ jobs: strategy: matrix: image: - - 'mathcomp/mathcomp:2.1.0-coq-8.16' - - 'mathcomp/mathcomp:2.1.0-coq-8.17' - - 'mathcomp/mathcomp:2.1.0-coq-8.18' - - 'mathcomp/mathcomp:2.2.0-coq-8.19' - - 'mathcomp/mathcomp-dev:coq-8.18' - - 'mathcomp/mathcomp-dev:coq-8.19' - 'mathcomp/mathcomp-dev:coq-dev' + - 'mathcomp/mathcomp-dev:coq-8.19' + - 'mathcomp/mathcomp-dev:coq-8.18' + - 'mathcomp/mathcomp:2.2.0-coq-8.19' + - 'mathcomp/mathcomp:2.1.0-coq-8.18' + - 'mathcomp/mathcomp:2.1.0-coq-8.17' + - 'mathcomp/mathcomp:2.1.0-coq-8.16' fail-fast: false steps: - uses: actions/checkout@v3 diff --git a/README.md b/README.md index ecb7e70..cf955b6 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/math-comp/abel/workflows/Docker%20CI/badge.svg?branch=master -[docker-action-link]: https://github.com/math-comp/abel/actions?query=workflow:"Docker%20CI" +[docker-action-shield]: https://github.com/math-comp/abel/actions/workflows/docker-action.yml/badge.svg?branch=master +[docker-action-link]: https://github.com/math-comp/abel/actions/workflows/docker-action.yml @@ -28,12 +28,12 @@ Mathematical Components library. - License: [CeCILL-B](CeCILL-B) - Compatible Coq versions: Coq 8.10 to 8.16 - Additional dependencies: - - [MathComp ssreflect 1.13 and later](https://math-comp.github.io) - - [MathComp fingroup 1.13 and later](https://math-comp.github.io) - - [MathComp algebra 1.13 and later](https://math-comp.github.io) - - [MathComp solvable 1.13 and later](https://math-comp.github.io) - - [MathComp field 1.13 and later](https://math-comp.github.io) - - [MathComp real closed >= 1.1.1](https://github.com/math-comp/real-closed) + - [MathComp ssreflect 2.0 and later](https://math-comp.github.io) + - [MathComp fingroup](https://math-comp.github.io) + - [MathComp algebra](https://math-comp.github.io) + - [MathComp solvable](https://math-comp.github.io) + - [MathComp field](https://math-comp.github.io) + - [MathComp real closed >= 2.0.0](https://github.com/math-comp/real-closed) - Coq namespace: `Abel` - Related publication(s): - [Unsolvability of the Quintic Formalized in Dependent Type Theory diff --git a/coq-mathcomp-abel.opam b/coq-mathcomp-abel.opam index 6f0fe0b..25eaf27 100644 --- a/coq-mathcomp-abel.opam +++ b/coq-mathcomp-abel.opam @@ -21,7 +21,7 @@ Mathematical Components library.""" build: [make "-j%{jobs}%"] install: [make "install"] depends: [ - "coq" { (>= "8.16" & < "8.20~") | = "dev" } + "coq" { (>= "8.10" & < "8.20~") | = "dev" } "coq-mathcomp-ssreflect" { (>= "2.0.0" & < "2.3~") | = "dev" } "coq-mathcomp-fingroup" "coq-mathcomp-algebra"