diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml index 78d4a0c..7f6e789 100644 --- a/.github/workflows/docker-action.yml +++ b/.github/workflows/docker-action.yml @@ -19,8 +19,13 @@ jobs: image: - 'mathcomp/mathcomp:2.0.0-coq-8.16' - 'mathcomp/mathcomp:2.0.0-coq-8.17' + - 'mathcomp/mathcomp:2.0.0-coq-8.18' + - '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-dev:coq-8.16' - 'mathcomp/mathcomp-dev:coq-8.17' + - 'mathcomp/mathcomp-dev:coq-8.18' - 'mathcomp/mathcomp-dev:coq-dev' fail-fast: false steps: diff --git a/README.md b/README.md index 823c77c..1d6af44 100644 --- a/README.md +++ b/README.md @@ -24,9 +24,9 @@ which will be used to subsume notations for finite sets, eventually. - Cyril Cohen (initial) - Kazuhiko Sakaguchi - License: [CeCILL-B](CECILL-B) -- Compatible Coq versions: Coq 8.13 to 8.16 +- Compatible Coq versions: Coq 8.16 to 8.18 - Additional dependencies: - - [MathComp ssreflect 1.13 to 1.15](https://math-comp.github.io) + - [MathComp ssreflect 2.0 to 2.1](https://math-comp.github.io) - Coq namespace: `mathcomp.finmap` - Related publication(s): none diff --git a/coq-mathcomp-finmap.opam b/coq-mathcomp-finmap.opam index 737d3be..3dc6914 100644 --- a/coq-mathcomp-finmap.opam +++ b/coq-mathcomp-finmap.opam @@ -21,8 +21,8 @@ which will be used to subsume notations for finite sets, eventually.""" build: [make "-j%{jobs}%"] install: [make "install"] depends: [ - "coq" { (>= "8.16" & < "8.18~") | (= "dev") } - "coq-mathcomp-ssreflect" { (>= "2.0.0" & < "2.1~") | (= "dev") } + "coq" { (>= "8.16" & < "8.19~") | (= "dev") } + "coq-mathcomp-ssreflect" { (>= "2.0" & < "2.2~") | (= "dev") } ] tags: [ diff --git a/meta.yml b/meta.yml index 77eb7a1..8b730ee 100644 --- a/meta.yml +++ b/meta.yml @@ -31,37 +31,27 @@ license: file: CECILL-B supported_coq_versions: - text: Coq 8.13 to 8.16 - opam: '{ (>= "8.13" & < "8.17~") | (= "dev") }' + text: Coq 8.16 to 8.18 + opam: '{ (>= "8.16" & < "8.19~") | (= "dev") }' tested_coq_opam_versions: -- version: '1.13.0-coq-8.13' +- version: '2.0.0-coq-8.16' repo: 'mathcomp/mathcomp' -- version: '1.13.0-coq-8.14' +- version: '2.0.0-coq-8.17' repo: 'mathcomp/mathcomp' -- version: '1.13.0-coq-8.15' +- version: '2.0.0-coq-8.18' repo: 'mathcomp/mathcomp' -- version: '1.14.0-coq-8.13' +- version: '2.1.0-coq-8.16' repo: 'mathcomp/mathcomp' -- version: '1.14.0-coq-8.14' +- version: '2.1.0-coq-8.17' repo: 'mathcomp/mathcomp' -- version: '1.14.0-coq-8.15' +- version: '2.1.0-coq-8.18' repo: 'mathcomp/mathcomp' -- version: '1.15.0-coq-8.13' - repo: 'mathcomp/mathcomp' -- version: '1.15.0-coq-8.14' - 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' +- version: 'coq-8.16' repo: 'mathcomp/mathcomp-dev' -- version: 'coq-8.15' +- version: 'coq-8.17' repo: 'mathcomp/mathcomp-dev' -- version: 'coq-8.16' +- version: 'coq-8.18' repo: 'mathcomp/mathcomp-dev' - version: 'coq-dev' repo: 'mathcomp/mathcomp-dev' @@ -69,9 +59,9 @@ tested_coq_opam_versions: dependencies: - opam: name: coq-mathcomp-ssreflect - version: '{ (>= "1.13.0" & < "1.16~") | (= "dev") }' + version: '{ (>= "2.0" & < "2.2~") | (= "dev") }' description: |- - [MathComp ssreflect 1.13 to 1.15](https://math-comp.github.io) + [MathComp ssreflect 2.0 to 2.1](https://math-comp.github.io) namespace: mathcomp.finmap