diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml index ca566b0..464a2ad 100644 --- a/.github/workflows/docker-action.yml +++ b/.github/workflows/docker-action.yml @@ -17,9 +17,9 @@ jobs: strategy: matrix: image: - - 'mathcomp/mathcomp:1.15.0-coq-8.15' - - 'mathcomp/mathcomp:1.17.0-coq-8.18' - - 'mathcomp/mathcomp-dev:coq-dev' + - 'mathcomp/mathcomp:2.2.0-coq-8.16' + - 'mathcomp/mathcomp:2.2.0-coq-8.19' + - 'mathcomp/mathcomp-dev:latest-coq-dev' fail-fast: false steps: - uses: actions/checkout@v3 diff --git a/README.md b/README.md index 144da15..8016fae 100644 --- a/README.md +++ b/README.md @@ -29,9 +29,9 @@ This library relies on propositional and functional extentionality axioms. - Anton Trunov - Alexander Gryzlov - License: [Apache-2.0](LICENSE) -- Compatible Coq versions: Coq 8.15 to 8.17 +- Compatible Coq versions: Coq 8.16 to 8.19 - Additional dependencies: - - [MathComp ssreflect 1.15 to 1.17](https://math-comp.github.io) + - [MathComp ssreflect 2.2](https://math-comp.github.io) - [MathComp algebra](https://math-comp.github.io) - Coq namespace: `pcm` - Related publication(s): none diff --git a/coq-fcsl-pcm.opam b/coq-fcsl-pcm.opam index 7a125ba..239e934 100644 --- a/coq-fcsl-pcm.opam +++ b/coq-fcsl-pcm.opam @@ -25,8 +25,8 @@ This library relies on propositional and functional extentionality axioms.""" build: [make "-j%{jobs}%"] install: [make "install"] depends: [ - "coq" { (>= "8.15" & < "8.19~") | (= "dev") } - "coq-mathcomp-ssreflect" { (>= "1.15.0" & < "1.18~") | (= "dev") } + "coq" { (>= "8.16" & < "8.20~") | (= "dev") } + "coq-mathcomp-ssreflect" { (>= "2.2.0" & < "2.3~") | (= "dev") } "coq-mathcomp-algebra" ] diff --git a/meta.yml b/meta.yml index d60bbc0..f38b091 100644 --- a/meta.yml +++ b/meta.yml @@ -40,23 +40,23 @@ license: file: LICENSE supported_coq_versions: - text: Coq 8.15 to 8.17 - opam: '{ (>= "8.15" & < "8.19~") | (= "dev") }' + text: Coq 8.16 to 8.19 + opam: '{ (>= "8.16" & < "8.20~") | (= "dev") }' tested_coq_opam_versions: -- version: '1.15.0-coq-8.15' +- version: '2.2.0-coq-8.16' repo: 'mathcomp/mathcomp' -- version: '1.17.0-coq-8.18' +- version: '2.2.0-coq-8.19' repo: 'mathcomp/mathcomp' -- version: 'coq-dev' +- version: 'latest-coq-dev' repo: 'mathcomp/mathcomp-dev' dependencies: - opam: name: coq-mathcomp-ssreflect - version: '{ (>= "1.15.0" & < "1.18~") | (= "dev") }' + version: '{ (>= "2.2.0" & < "2.3~") | (= "dev") }' description: |- - [MathComp ssreflect 1.15 to 1.17](https://math-comp.github.io) + [MathComp ssreflect 2.2](https://math-comp.github.io) - opam: name: coq-mathcomp-algebra description: |-