coq 8.17 mathcomp 1.17

thery · Jun 14, 2023 · 5a7029d · 5a7029d
1 parent b72bfbf
commit 5a7029d
Show file tree

Hide file tree

Showing 4 changed files with 10 additions and 10 deletions.
diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml
@@ -17,7 +17,7 @@ jobs:
     strategy:
       matrix:
         image:
-          - 'mathcomp/mathcomp:1.16.0-coq-8.16'
+          - 'mathcomp/mathcomp:1.16.0-coq-8.17'
       fail-fast: false
     steps:
       - uses: actions/checkout@v3

diff --git a/README.md b/README.md
@@ -20,9 +20,9 @@ Following The Group Law for Edwards Curves Thomas C. Hales
 - Author(s):
   - Laurent Théry
 - License: [MIT License](LICENSE)
-- Compatible Coq versions: 8.16 or later
+- Compatible Coq versions: 8.17 or later
 - Additional dependencies:
-  - [MathComp ssreflect 1.16 or later](https://math-comp.github.io)
+  - [MathComp ssreflect 1.17 or later](https://math-comp.github.io)
 - Coq namespace: `edwards`
 - Related publication(s): none
 

diff --git a/coq-edwards.opam b/coq-edwards.opam
@@ -18,8 +18,8 @@ Following The Group Law for Edwards Curves Thomas C. Hales"""
 build: [make "-j%{jobs}%"]
 install: [make "install"]
 depends: [
-  "coq" {(>= "8.16")}
-  "coq-mathcomp-ssreflect" {(>= "1.16.0")}
+  "coq" {(>= "8.17")}
+  "coq-mathcomp-ssreflect" {(>= "1.17.0")}
 ]
 
 tags: [

diff --git a/meta.yml b/meta.yml
@@ -27,18 +27,18 @@ license:
   identifier: MIT
 
 supported_coq_versions:
-  text: '8.16 or later'
-  opam: '{(>= "8.16")}'
+  text: '8.17 or later'
+  opam: '{(>= "8.17")}'
 
 dependencies:
 - opam:
     name: coq-mathcomp-ssreflect
-    version: '{(>= "1.16.0")}'
+    version: '{(>= "1.17.0")}'
   description: |-
-    [MathComp ssreflect 1.16 or later](https://math-comp.github.io)
+    [MathComp ssreflect 1.17 or later](https://math-comp.github.io)
 
 tested_coq_opam_versions:
-- version: '1.16.0-coq-8.16'
+- version: '1.16.0-coq-8.17'
   repo: 'mathcomp/mathcomp'
 
 namespace: edwards