Merge pull request #65 from proux01/coq_816

[CI] Add Coq 8.16 and MC 1.15

.github/workflows/docker-action.yml

@@ -17,20 +17,18 @@ jobs:
     strategy:
       matrix:
         image:
+          - 'mathcomp/mathcomp:1.15.0-coq-8.16'
+          - 'mathcomp/mathcomp:1.15.0-coq-8.15'
+          - 'mathcomp/mathcomp:1.15.0-coq-8.14'
+          - 'mathcomp/mathcomp:1.15.0-coq-8.13'
           - 'mathcomp/mathcomp:1.14.0-coq-8.15'
           - 'mathcomp/mathcomp:1.14.0-coq-8.14'
           - 'mathcomp/mathcomp:1.14.0-coq-8.13'
-          - 'mathcomp/mathcomp:1.14.0-coq-8.12'
-          - 'mathcomp/mathcomp:1.14.0-coq-8.11'
           - 'mathcomp/mathcomp:1.13.0-coq-8.15'
           - 'mathcomp/mathcomp:1.13.0-coq-8.14'
           - 'mathcomp/mathcomp:1.13.0-coq-8.13'
-          - 'mathcomp/mathcomp:1.13.0-coq-8.12'
-          - 'mathcomp/mathcomp:1.13.0-coq-8.11'
           - 'mathcomp/mathcomp-dev:coq-dev'
-          - 'mathcomp/mathcomp-dev:coq-8.15'
-          - 'mathcomp/mathcomp-dev:coq-8.14'
-          - 'mathcomp/mathcomp-dev:coq-8.13'
+          - 'mathcomp/mathcomp-dev:coq-8.16'
       fail-fast: false
     steps:
       - uses: actions/checkout@v2

README.md

@@ -44,7 +44,7 @@ of the ForMath EU FP7 project (2009-2013). It has two parts:
   - Cyril Cohen ([**@CohenCyril**](https://github.com/CohenCyril))
   - Pierre Roux ([**@proux01**](https://github.com/proux01))
 - License: [MIT License](LICENSE)
-- Compatible Coq versions: 8.10 or later (use releases for other Coq versions)
+- Compatible Coq versions: 8.13 or later (use releases for other Coq versions)
 - Additional dependencies:
   - [Bignums](https://github.com/coq/bignums) same version as Coq
   - [Paramcoq](https://github.com/coq-community/paramcoq) 1.1.3 or later

coq-coqeal.opam

@@ -21,11 +21,11 @@ of the ForMath EU FP7 project (2009-2013). It has two parts:
 build: [make "-j%{jobs}%"]
 install: [make "install"]
 depends: [
-  "coq" {(>= "8.10" & < "8.16~") | (= "dev")}
+  "coq" {(>= "8.13" & < "8.17~") | (= "dev")}
   "coq-bignums" 
   "coq-paramcoq" {>= "1.1.3"}
   "coq-mathcomp-multinomials" {((>= "1.5.1" & < "1.7~") | = "dev")}
-  "coq-mathcomp-algebra" {((>= "1.13.0" & < "1.15~") | = "dev")}
+  "coq-mathcomp-algebra" {((>= "1.13.0" & < "1.16~") | = "dev")}
   "coq-mathcomp-real-closed" {(>= "1.1.2" & < "1.2~") | (= "dev")}
 ]
 

meta.yml

@@ -68,8 +68,8 @@ license:
   identifier: MIT
 
 supported_coq_versions:
-  text: 8.10 or later (use releases for other Coq versions)
-  opam: '{(>= "8.10" & < "8.16~") | (= "dev")}'
+  text: 8.13 or later (use releases for other Coq versions)
+  opam: '{(>= "8.13" & < "8.17~") | (= "dev")}'
 
 dependencies:
 - opam:
@@ -88,7 +88,7 @@ dependencies:
     [MathComp Multinomials](https://github.com/math-comp/multinomials) >= 1.5.1 and < 1.7
 - opam:
     name: coq-mathcomp-algebra
-    version: '{((>= "1.13.0" & < "1.15~") | = "dev")}'
+    version: '{((>= "1.13.0" & < "1.16~") | = "dev")}'
   description: |-
     [MathComp algebra](https://math-comp.github.io) 1.13.0 or later
 - opam:
@@ -98,33 +98,29 @@ dependencies:
     [MathComp real-closed](https://math-comp.github.io) 1.1.2 or later
 
 tested_coq_opam_versions:
+- version: '1.15.0-coq-8.16'
+  repo: 'mathcomp/mathcomp'
+- version: '1.15.0-coq-8.15'
+  repo: 'mathcomp/mathcomp'
+- version: '1.15.0-coq-8.14'
+  repo: 'mathcomp/mathcomp'
+- version: '1.15.0-coq-8.13'
+  repo: 'mathcomp/mathcomp'
 - version: '1.14.0-coq-8.15'
   repo: 'mathcomp/mathcomp'
 - version: '1.14.0-coq-8.14'
   repo: 'mathcomp/mathcomp'
 - version: '1.14.0-coq-8.13'
   repo: 'mathcomp/mathcomp'
-- version: '1.14.0-coq-8.12'
-  repo: 'mathcomp/mathcomp'
-- version: '1.14.0-coq-8.11'
-  repo: 'mathcomp/mathcomp'
 - version: '1.13.0-coq-8.15'
   repo: 'mathcomp/mathcomp'
 - version: '1.13.0-coq-8.14'
   repo: 'mathcomp/mathcomp'
 - version: '1.13.0-coq-8.13'
   repo: 'mathcomp/mathcomp'
-- version: '1.13.0-coq-8.12'
-  repo: 'mathcomp/mathcomp'
-- version: '1.13.0-coq-8.11'
-  repo: 'mathcomp/mathcomp'
 - version: 'coq-dev'
   repo: 'mathcomp/mathcomp-dev'
-- version: 'coq-8.15'
-  repo: 'mathcomp/mathcomp-dev'
-- version: 'coq-8.14'
-  repo: 'mathcomp/mathcomp-dev'
-- version: 'coq-8.13'
+- version: 'coq-8.16'
   repo: 'mathcomp/mathcomp-dev'
 
 namespace: CoqEAL