diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml index 71f6b73..137c7d5 100644 --- a/.github/workflows/docker-action.yml +++ b/.github/workflows/docker-action.yml @@ -28,9 +28,11 @@ jobs: - 'mathcomp/mathcomp:1.14.0-coq-8.14' - 'mathcomp/mathcomp:1.15.0-coq-8.14' - 'mathcomp/mathcomp:1.15.0-coq-8.15' + - 'mathcomp/mathcomp:1.15.0-coq-8.16' - 'mathcomp/mathcomp-dev:coq-8.13' - 'mathcomp/mathcomp-dev:coq-8.14' - 'mathcomp/mathcomp-dev:coq-8.15' + - 'mathcomp/mathcomp-dev:coq-8.16' - 'mathcomp/mathcomp-dev:coq-dev' fail-fast: false steps: diff --git a/README.md b/README.md index 997c6c4..a93d46c 100644 --- a/README.md +++ b/README.md @@ -26,7 +26,7 @@ Mathematical Components library. - Assia Mahboubi (initial) - Pierre-Yves Strub (initial) - License: [CeCILL-B](CeCILL-B) -- Compatible Coq versions: Coq 8.10 to 8.15 +- Compatible Coq versions: Coq 8.10 to 8.16 - Additional dependencies: - [MathComp ssreflect 1.12 and later](https://math-comp.github.io) - [MathComp fingroup 1.12 and later](https://math-comp.github.io) diff --git a/coq-mathcomp-abel.opam b/coq-mathcomp-abel.opam index 1b9b321..1864194 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.10" & < "8.16~") | = "dev" } + "coq" { (>= "8.10" & < "8.17~") | = "dev" } "coq-mathcomp-ssreflect" { (>= "1.12.0" & < "1.16~") | = "dev" } "coq-mathcomp-fingroup" "coq-mathcomp-algebra" diff --git a/meta.yml b/meta.yml index 6c7b5e5..7765d2e 100644 --- a/meta.yml +++ b/meta.yml @@ -41,8 +41,8 @@ license: file: CeCILL-B supported_coq_versions: - text: Coq 8.10 to 8.15 - opam: '{ (>= "8.10" & < "8.16~") | = "dev" }' + text: Coq 8.10 to 8.16 + opam: '{ (>= "8.10" & < "8.17~") | = "dev" }' tested_coq_opam_versions: - version: '1.12.0-coq-8.10' @@ -67,12 +67,16 @@ tested_coq_opam_versions: repo: 'mathcomp/mathcomp' - version: '1.15.0-coq-8.15' repo: 'mathcomp/mathcomp' +- version: '1.15.0-coq-8.16' + repo: 'mathcomp/mathcomp' - version: 'coq-8.13' repo: 'mathcomp/mathcomp-dev' - version: 'coq-8.14' repo: 'mathcomp/mathcomp-dev' - version: 'coq-8.15' repo: 'mathcomp/mathcomp-dev' +- version: 'coq-8.16' + repo: 'mathcomp/mathcomp-dev' - version: 'coq-dev' repo: 'mathcomp/mathcomp-dev'