Skip to content

Commit 61d79ae

Browse files
authored
Merge pull request #78 from math-comp/update
Add Coq 8.16 to docker actions too
2 parents 2e78602 + 4d0fb51 commit 61d79ae

File tree

4 files changed

+10
-4
lines changed

4 files changed

+10
-4
lines changed

.github/workflows/docker-action.yml

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -28,9 +28,11 @@ jobs:
2828
- 'mathcomp/mathcomp:1.14.0-coq-8.14'
2929
- 'mathcomp/mathcomp:1.15.0-coq-8.14'
3030
- 'mathcomp/mathcomp:1.15.0-coq-8.15'
31+
- 'mathcomp/mathcomp:1.15.0-coq-8.16'
3132
- 'mathcomp/mathcomp-dev:coq-8.13'
3233
- 'mathcomp/mathcomp-dev:coq-8.14'
3334
- 'mathcomp/mathcomp-dev:coq-8.15'
35+
- 'mathcomp/mathcomp-dev:coq-8.16'
3436
- 'mathcomp/mathcomp-dev:coq-dev'
3537
fail-fast: false
3638
steps:

README.md

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -26,7 +26,7 @@ Mathematical Components library.
2626
- Assia Mahboubi (initial)
2727
- Pierre-Yves Strub (initial)
2828
- License: [CeCILL-B](CeCILL-B)
29-
- Compatible Coq versions: Coq 8.10 to 8.15
29+
- Compatible Coq versions: Coq 8.10 to 8.16
3030
- Additional dependencies:
3131
- [MathComp ssreflect 1.12 and later](https://math-comp.github.io)
3232
- [MathComp fingroup 1.12 and later](https://math-comp.github.io)

coq-mathcomp-abel.opam

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -21,7 +21,7 @@ Mathematical Components library."""
2121
build: [make "-j%{jobs}%"]
2222
install: [make "install"]
2323
depends: [
24-
"coq" { (>= "8.10" & < "8.16~") | = "dev" }
24+
"coq" { (>= "8.10" & < "8.17~") | = "dev" }
2525
"coq-mathcomp-ssreflect" { (>= "1.12.0" & < "1.16~") | = "dev" }
2626
"coq-mathcomp-fingroup"
2727
"coq-mathcomp-algebra"

meta.yml

Lines changed: 6 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -41,8 +41,8 @@ license:
4141
file: CeCILL-B
4242

4343
supported_coq_versions:
44-
text: Coq 8.10 to 8.15
45-
opam: '{ (>= "8.10" & < "8.16~") | = "dev" }'
44+
text: Coq 8.10 to 8.16
45+
opam: '{ (>= "8.10" & < "8.17~") | = "dev" }'
4646

4747
tested_coq_opam_versions:
4848
- version: '1.12.0-coq-8.10'
@@ -67,12 +67,16 @@ tested_coq_opam_versions:
6767
repo: 'mathcomp/mathcomp'
6868
- version: '1.15.0-coq-8.15'
6969
repo: 'mathcomp/mathcomp'
70+
- version: '1.15.0-coq-8.16'
71+
repo: 'mathcomp/mathcomp'
7072
- version: 'coq-8.13'
7173
repo: 'mathcomp/mathcomp-dev'
7274
- version: 'coq-8.14'
7375
repo: 'mathcomp/mathcomp-dev'
7476
- version: 'coq-8.15'
7577
repo: 'mathcomp/mathcomp-dev'
78+
- version: 'coq-8.16'
79+
repo: 'mathcomp/mathcomp-dev'
7680
- version: 'coq-dev'
7781
repo: 'mathcomp/mathcomp-dev'
7882

0 commit comments

Comments
 (0)