Update versions

Author: ablearthy

.github/workflows/docker-action.yml

@@ -17,12 +17,11 @@ jobs:
     strategy:
       matrix:
         image:
-          - 'mathcomp/mathcomp:1.19.0-coq-8.20'
-          - 'mathcomp/mathcomp:1.19.0-coq-8.19'
-          - 'mathcomp/mathcomp:1.18.0-coq-8.18'
-          - 'mathcomp/mathcomp:1.17.0-coq-8.17'
-          - 'mathcomp/mathcomp:1.17.0-coq-8.16'
-          - 'mathcomp/mathcomp:1.17.0-coq-8.15'
+          - '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

README.md

@@ -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.15 to 8.19
+- Compatible Coq versions: 8.16 to 8.20
 - Additional dependencies:
-  - [MathComp ssreflect](https://math-comp.github.io) 1.17.0 to 1.19.0
+  - [MathComp ssreflect](https://math-comp.github.io) 2.2 to 2.3
   - [MathComp algebra](https://math-comp.github.io)
   - [Equations](https://github.com/mattam82/Coq-Equations) 1.3 or later
 - Coq namespace: `favssr`

coq-fav-ssr.opam

@@ -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.15" & < "8.21"}
-  "coq-mathcomp-ssreflect" {>= "1.17" & < "2.0"}
+  "coq" {>= "8.16" & < "8.21"}
+  "coq-mathcomp-ssreflect" {>= "2.2" & < "2.4"}
   "coq-mathcomp-algebra" 
   "coq-equations" {>= "1.3"}
 ]

meta.yml

@@ -32,27 +32,27 @@ license:
   identifier: MIT
 
 supported_coq_versions:
-  text: 8.15 to 8.20
-  opam: '{>= "8.15" & < "8.21"}'
+  text: 8.16 to 8.20
+  opam: '{>= "8.16" & < "8.21"}'
 
 tested_coq_opam_versions:
-- version: '1.19.0-coq-8.19'
+- version: '2.3.0-coq-8.20'
   repo: 'mathcomp/mathcomp'
-- version: '1.18.0-coq-8.18'
+- version: '2.3.0-coq-8.19'
   repo: 'mathcomp/mathcomp'
-- version: '1.17.0-coq-8.17'
+- version: '2.3.0-coq-8.18'
   repo: 'mathcomp/mathcomp'
-- version: '1.17.0-coq-8.16'
+- version: '2.2.0-coq-8.17'
   repo: 'mathcomp/mathcomp'
-- version: '1.17.0-coq-8.15'
+- version: '2.2.0-coq-8.16'
   repo: 'mathcomp/mathcomp'
 
 dependencies:
 - opam:
     name: coq-mathcomp-ssreflect
-    version: '{>= "1.17" & < "2.0"}'
+    version: '{>= "2.2" & <= "2.3"}'
   description: |-
-    [MathComp ssreflect](https://math-comp.github.io) 1.17.0 to 1.19.0
+    [MathComp ssreflect](https://math-comp.github.io) 2.2 to 2.3
 - opam:
     name: coq-mathcomp-algebra
   description: |-