Update Docker CI and README

.github/workflows/docker-action.yml

@@ -19,8 +19,18 @@ jobs:
         image:
           - 'mathcomp/mathcomp:2.0.0-coq-8.16'
           - 'mathcomp/mathcomp:2.0.0-coq-8.17'
-          - 'mathcomp/mathcomp-dev:coq-8.16'
+          - 'mathcomp/mathcomp:2.0.0-coq-8.18'
+          - 'mathcomp/mathcomp:2.1.0-coq-8.16'
+          - 'mathcomp/mathcomp:2.1.0-coq-8.17'
+          - 'mathcomp/mathcomp:2.1.0-coq-8.18'
+          - 'mathcomp/mathcomp:2.2.0-coq-8.16'
+          - 'mathcomp/mathcomp:2.2.0-coq-8.17'
+          - 'mathcomp/mathcomp:2.2.0-coq-8.18'
+          - 'mathcomp/mathcomp:2.2.0-coq-8.19'
+          - 'mathcomp/mathcomp:2.2.0-coq-dev'
           - 'mathcomp/mathcomp-dev:coq-8.17'
+          - 'mathcomp/mathcomp-dev:coq-8.18'
+          - 'mathcomp/mathcomp-dev:coq-8.19'
           - 'mathcomp/mathcomp-dev:coq-dev'
       fail-fast: false
     steps:

README.md

@@ -6,8 +6,8 @@ Follow the instructions on https://github.com/coq-community/templates to regener
 
 [![Docker CI][docker-action-shield]][docker-action-link]
 
-[docker-action-shield]: https://github.com/math-comp/real-closed/workflows/Docker%20CI/badge.svg?branch=master
-[docker-action-link]: https://github.com/math-comp/real-closed/actions?query=workflow:"Docker%20CI"
+[docker-action-shield]: https://github.com/math-comp/real-closed/actions/workflows/docker-action.yml/badge.svg?branch=master
+[docker-action-link]: https://github.com/math-comp/real-closed/actions/workflows/docker-action.yml
 
 
 
@@ -24,11 +24,11 @@ order theory of real closed field, through quantifier elimination.
   - Cyril Cohen (initial)
   - Assia Mahboubi (initial)
 - License: [CeCILL-B](CECILL-B)
-- Compatible Coq versions: Coq 8.13 or later
+- Compatible Coq versions: Coq 8.16 or later
 - Additional dependencies:
-  - [MathComp ssreflect 1.13 or later](https://math-comp.github.io)
-  - [MathComp algebra 1.13 or later](https://math-comp.github.io)
-  - [MathComp field 1.13 or later](https://math-comp.github.io)
+  - [MathComp ssreflect 2.0 or later](https://math-comp.github.io)
+  - [MathComp algebra](https://math-comp.github.io)
+  - [MathComp field](https://math-comp.github.io)
   - [MathComp bigenough 1.0.0 or later](https://github.com/math-comp/bigenough)
 - Coq namespace: `mathcomp.real_closed`
 - Related publication(s):

coq-mathcomp-real-closed.opam

@@ -22,9 +22,9 @@ build: [make "-j%{jobs}%"]
 install: [make "install"]
 depends: [
   "coq" {>= "8.16"}
-  "coq-mathcomp-ssreflect" {>= "2.0.0"}
-  "coq-mathcomp-algebra"
-  "coq-mathcomp-field"
+  "coq-mathcomp-ssreflect" {>= "2.0"}
+  "coq-mathcomp-algebra" 
+  "coq-mathcomp-field" 
   "coq-mathcomp-bigenough" {>= "1.0.0"}
 ]
 

meta.yml

@@ -39,53 +39,55 @@ license:
   file: CECILL-B
 
 supported_coq_versions:
-  text: Coq 8.13 or later
-  opam: '{>= "8.13"}'
+  text: Coq 8.16 or later
+  opam: '{>= "8.16"}'
 
 tested_coq_opam_versions:
-- version: '1.13.0-coq-8.13'
+- version: '2.0.0-coq-8.16'
   repo: 'mathcomp/mathcomp'
-- version: '1.13.0-coq-8.14'
+- version: '2.0.0-coq-8.17'
   repo: 'mathcomp/mathcomp'
-- version: '1.13.0-coq-8.15'
+- version: '2.0.0-coq-8.18'
   repo: 'mathcomp/mathcomp'
-- version: '1.14.0-coq-8.13'
+- version: '2.1.0-coq-8.16'
   repo: 'mathcomp/mathcomp'
-- version: '1.14.0-coq-8.14'
+- version: '2.1.0-coq-8.17'
   repo: 'mathcomp/mathcomp'
-- version: '1.14.0-coq-8.15'
+- version: '2.1.0-coq-8.18'
   repo: 'mathcomp/mathcomp'
-- version: '1.15.0-coq-8.13'
+- version: '2.2.0-coq-8.16'
   repo: 'mathcomp/mathcomp'
-- version: '1.15.0-coq-8.14'
+- version: '2.2.0-coq-8.17'
   repo: 'mathcomp/mathcomp'
-- version: '1.15.0-coq-8.15'
+- version: '2.2.0-coq-8.18'
   repo: 'mathcomp/mathcomp'
-- version: 'coq-8.13'
+- version: '2.2.0-coq-8.19'
+  repo: 'mathcomp/mathcomp'
+- version: '2.2.0-coq-dev'
+  repo: 'mathcomp/mathcomp'
+- version: 'coq-8.17'
   repo: 'mathcomp/mathcomp-dev'
-- version: 'coq-8.14'
+- version: 'coq-8.18'
   repo: 'mathcomp/mathcomp-dev'
-- version: 'coq-8.15'
+- version: 'coq-8.19'
   repo: 'mathcomp/mathcomp-dev'
 - version: 'coq-dev'
   repo: 'mathcomp/mathcomp-dev'
 
 dependencies:
 - opam:
     name: coq-mathcomp-ssreflect
-    version: '{>= "1.13.0"}'
+    version: '{>= "2.0"}'
   description: |-
-    [MathComp ssreflect 1.13 or later](https://math-comp.github.io)
+    [MathComp ssreflect 2.0 or later](https://math-comp.github.io)
 - opam:
     name: coq-mathcomp-algebra
-    version: '{>= "1.13.0"}'
   description: |-
-    [MathComp algebra 1.13 or later](https://math-comp.github.io)
+    [MathComp algebra](https://math-comp.github.io)
 - opam:
     name: coq-mathcomp-field
-    version: '{>= "1.13.0"}'
   description: |-
-    [MathComp field 1.13 or later](https://math-comp.github.io)
+    [MathComp field](https://math-comp.github.io)
 - opam:
     name: coq-mathcomp-bigenough
     version: '{>= "1.0.0"}'