Skip to content

Commit

Permalink
Remove mathcomp 2.2
Browse files Browse the repository at this point in the history
  • Loading branch information
ablearthy committed Jan 5, 2025
1 parent d272f37 commit 3998099
Show file tree
Hide file tree
Showing 4 changed files with 8 additions and 14 deletions.
2 changes: 0 additions & 2 deletions .github/workflows/docker-action.yml
Original file line number Diff line number Diff line change
Expand Up @@ -20,8 +20,6 @@ jobs:
- 'mathcomp/mathcomp:2.3.0-coq-8.20'
- 'mathcomp/mathcomp:2.3.0-coq-8.19'
- 'mathcomp/mathcomp:2.3.0-coq-8.18'
- 'mathcomp/mathcomp:2.2.0-coq-8.17'
- 'mathcomp/mathcomp:2.2.0-coq-8.16'
fail-fast: false
steps:
- uses: actions/checkout@v3
Expand Down
4 changes: 2 additions & 2 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -34,9 +34,9 @@ The book was previously called "Functional Algorithms Verified", hence the FAV a
- Coq-community maintainer(s):
- Alex Gryzlov ([**@clayrat**](https://github.com/clayrat))
- License: [MIT license](LICENSE)
- Compatible Coq versions: 8.16 to 8.20
- Compatible Coq versions: 8.18 to 8.20
- Additional dependencies:
- [MathComp ssreflect](https://math-comp.github.io) 2.2 to 2.3
- [MathComp ssreflect](https://math-comp.github.io) 2.3
- [MathComp algebra](https://math-comp.github.io)
- [Equations](https://github.com/mattam82/Coq-Equations) 1.3 or later
- Coq namespace: `favssr`
Expand Down
4 changes: 2 additions & 2 deletions coq-fav-ssr.opam
Original file line number Diff line number Diff line change
Expand Up @@ -19,8 +19,8 @@ The book was previously called "Functional Algorithms Verified", hence the FAV a
build: [make "-j%{jobs}%"]
install: [make "install"]
depends: [
"coq" {>= "8.16" & < "8.21"}
"coq-mathcomp-ssreflect" {>= "2.2" & < "2.4"}
"coq" {>= "8.18" & < "8.21"}
"coq-mathcomp-ssreflect" {>= "2.3" & < "2.4"}
"coq-mathcomp-algebra"
"coq-equations" {>= "1.3"}
]
Expand Down
12 changes: 4 additions & 8 deletions meta.yml
Original file line number Diff line number Diff line change
Expand Up @@ -32,8 +32,8 @@ license:
identifier: MIT

supported_coq_versions:
text: 8.16 to 8.20
opam: '{>= "8.16" & < "8.21"}'
text: 8.18 to 8.20
opam: '{>= "8.18" & < "8.21"}'

tested_coq_opam_versions:
- version: '2.3.0-coq-8.20'
Expand All @@ -42,17 +42,13 @@ tested_coq_opam_versions:
repo: 'mathcomp/mathcomp'
- version: '2.3.0-coq-8.18'
repo: 'mathcomp/mathcomp'
- version: '2.2.0-coq-8.17'
repo: 'mathcomp/mathcomp'
- version: '2.2.0-coq-8.16'
repo: 'mathcomp/mathcomp'

dependencies:
- opam:
name: coq-mathcomp-ssreflect
version: '{>= "2.2" & < "2.4"}'
version: '{>= "2.3" & < "2.4"}'
description: |-
[MathComp ssreflect](https://math-comp.github.io) 2.2 to 2.3
[MathComp ssreflect](https://math-comp.github.io) 2.3.0
- opam:
name: coq-mathcomp-algebra
description: |-
Expand Down

0 comments on commit 3998099

Please sign in to comment.