coq 8.17 mathcomp 1.17

.github/workflows/docker-action.yml

@@ -17,7 +17,7 @@ jobs:
     strategy:
       matrix:
         image:
-          - 'mathcomp/mathcomp:1.16.0-coq-8.16'
+          - 'mathcomp/mathcomp:1.17.0-coq-8.17'
       fail-fast: false
     steps:
       - uses: actions/checkout@v3

README.md

@@ -27,9 +27,9 @@ It contains
 - Author(s):
   - Laurent Théry
 - License: [MIT License](LICENSE)
-- Compatible Coq versions: 8.15 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: `tutorial_material`
 - Related publication(s): none
 

Ssreflect15min/quesako.v

@@ -60,7 +60,7 @@ already require thinking a bit about data-structures and complexity. *)
 Close Scope Z_scope.
 
 (* E.g. unary numbes are not an option. *)
-Fail Eval compute in (1000 * 1000 : nat).
+Fail Eval compute in (10000 * 10000 : nat).
 
 (* A reflection-based tactic replace explicit deduction steps, 
 logged in proof terms, with computational steps, checked by the kernel's 

coq-tutorial_material.opam

@@ -25,8 +25,8 @@ It contains
 build: [make "-j%{jobs}%"]
 install: [make "install"]
 depends: [
-  "coq" {(>= "8.15")}
-  "coq-mathcomp-ssreflect" {(>= "1.16.0")}
+  "coq" {(>= "8.17")}
+  "coq-mathcomp-ssreflect" {(>= "1.17.0")}
 ]
 
 tags: [

meta.yml

@@ -34,18 +34,18 @@ license:
   identifier: MIT
 
 supported_coq_versions:
-  text: '8.15 or later'
-  opam: '{(>= "8.15")}'
+  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.17.0-coq-8.17'
   repo: 'mathcomp/mathcomp'
 
 namespace: tutorial_material