check with recent versions of Coq and MathComp

.github/workflows/docker-action.yml

@@ -19,6 +19,10 @@ jobs:
         image:
           - 'mathcomp/mathcomp:1.13.0-coq-8.13'
           - 'mathcomp/mathcomp:1.13.0-coq-8.14'
+          - 'mathcomp/mathcomp:1.13.0-coq-8.15'
+          - 'mathcomp/mathcomp:1.14.0-coq-8.13'
+          - 'mathcomp/mathcomp:1.14.0-coq-8.14'
+          - 'mathcomp/mathcomp:1.14.0-coq-8.15'
       fail-fast: false
     steps:
       - uses: actions/checkout@v2

README.md

@@ -71,7 +71,7 @@ make install
 
 ## Acknowledgments
 
-Many thanks to several contributors ([committers](https://github.com/affeldt-aist/infotheo/graphs/contributors)).
+Many thanks to several [contributors](https://github.com/affeldt-aist/infotheo/graphs/contributors).
 
 The principle of inclusion-exclusion is a contribution by 
 Erik Martin-Dorel (University Toulouse III Paul Sabatier, IRIT research laboratory)

coq-infotheo.opam

@@ -21,12 +21,12 @@ build: [
 ]
 install: [make "install"]
 depends: [
-  "coq" { (>= "8.13" & < "8.15~") | (= "dev") }
-  "coq-mathcomp-ssreflect" { (>= "1.13.0" & < "1.14~") | (= "dev") }
-  "coq-mathcomp-fingroup" { (>= "1.13.0" & < "1.14~") | (= "dev")  }
-  "coq-mathcomp-algebra" { (>= "1.13.0" & < "1.14~") | (= "dev")  }
-  "coq-mathcomp-solvable" { (>= "1.13.0" & < "1.14~") | (= "dev")  }
-  "coq-mathcomp-field" { (>= "1.13.0" & < "1.14~") | (= "dev")  }
+  "coq" { (>= "8.13" & < "8.16~") | (= "dev") }
+  "coq-mathcomp-ssreflect" { (>= "1.13.0" & < "1.15~") | (= "dev") }
+  "coq-mathcomp-fingroup" { (>= "1.13.0" & < "1.15~") | (= "dev")  }
+  "coq-mathcomp-algebra" { (>= "1.13.0" & < "1.15~") | (= "dev")  }
+  "coq-mathcomp-solvable" { (>= "1.13.0" & < "1.15~") | (= "dev")  }
+  "coq-mathcomp-field" { (>= "1.13.0" & < "1.15~") | (= "dev")  }
   "coq-mathcomp-analysis" { (>= "0.3.11") & (< "0.4~")}
 ]
 

meta.yml

@@ -42,38 +42,46 @@ nix: true
 
 supported_coq_versions:
   text: Coq 8.13, Coq 8.14
-  opam: '{ (>= "8.13" & < "8.15~") | (= "dev") }'
+  opam: '{ (>= "8.13" & < "8.16~") | (= "dev") }'
 
 tested_coq_opam_versions:
 - version: '1.13.0-coq-8.13'
   repo: 'mathcomp/mathcomp'
 - version: '1.13.0-coq-8.14'
   repo: 'mathcomp/mathcomp'
+- version: '1.13.0-coq-8.15'
+  repo: 'mathcomp/mathcomp'
+- version: '1.14.0-coq-8.13'
+  repo: 'mathcomp/mathcomp'
+- version: '1.14.0-coq-8.14'
+  repo: 'mathcomp/mathcomp'
+- version: '1.14.0-coq-8.15'
+  repo: 'mathcomp/mathcomp'
 
 dependencies:
 - opam:
     name: coq-mathcomp-ssreflect
-    version: '{ (>= "1.13.0" & < "1.14~") | (= "dev") }'
+    version: '{ (>= "1.13.0" & < "1.15~") | (= "dev") }'
   description: |-
     [MathComp ssreflect](https://math-comp.github.io)
 - opam:
     name: coq-mathcomp-fingroup
-    version: '{ (>= "1.13.0" & < "1.14~") | (= "dev")  }'
+    version: '{ (>= "1.13.0" & < "1.15~") | (= "dev")  }'
   description: |-
     [MathComp fingroup](https://math-comp.github.io)
 - opam:
     name: coq-mathcomp-algebra
-    version: '{ (>= "1.13.0" & < "1.14~") | (= "dev")  }'
+    version: '{ (>= "1.13.0" & < "1.15~") | (= "dev")  }'
   description: |-
     [MathComp algebra](https://math-comp.github.io)
 - opam:
     name: coq-mathcomp-solvable
-    version: '{ (>= "1.13.0" & < "1.14~") | (= "dev")  }'
+    version: '{ (>= "1.13.0" & < "1.15~") | (= "dev")  }'
   description: |-
     [MathComp solvable](https://math-comp.github.io)
 - opam:
     name: coq-mathcomp-field
-    version: '{ (>= "1.13.0" & < "1.14~") | (= "dev")  }'
+    version: '{ (>= "1.13.0" & < "1.15~") | (= "dev")  }'
   description: |-
     [MathComp field](https://math-comp.github.io)
 - opam: