Drop Coq 8.14 and MC 1.15 and 1.16 support

.github/workflows/docker-action.yml

@@ -15,13 +15,10 @@ jobs:
     strategy:
       matrix:
         image:
-          - 'mathcomp/mathcomp:1.15.0-coq-8.14'
-          - 'mathcomp/mathcomp:1.15.0-coq-8.15'
-          - 'mathcomp/mathcomp:1.15.0-coq-8.16'
-          - 'mathcomp/mathcomp:1.16.0-coq-8.14'
           - 'mathcomp/mathcomp:1.17.0-coq-8.15'
           - 'mathcomp/mathcomp:1.17.0-coq-8.16'
           - 'mathcomp/mathcomp:1.17.0-coq-8.17'
+          - 'mathcomp/mathcomp:1.18.0-coq-8.18'
       fail-fast: false
     steps:
       - uses: actions/checkout@v2

.nix/config.nix

@@ -37,7 +37,6 @@
   ## alternative configuration
   ## When generating GitHub Action CI, one workflow file
   ## will be created per bundle
-  bundles."8.14".coqPackages.coq.override.version = "8.14";
   bundles."8.15".coqPackages.coq.override.version = "8.15";
   bundles."8.16".push-branches = [ "master" "hierarchy-builder" ];
   bundles."8.16".coqPackages.coq.override.version = "8.16";

INSTALL.md

@@ -2,9 +2,9 @@
 
 ## Requirements
 
-- [The Coq Proof Assistant version ≥ 8.14](https://coq.inria.fr)
+- [The Coq Proof Assistant version ≥ 8.15](https://coq.inria.fr)
 - [Mathematical Components version ≥ 1.13.0](https://github.com/math-comp/math-comp)
-  + except `coq-mathcomp-solvable` ≥ 1.15.0
+  + except `coq-mathcomp-solvable` ≥ 1.17.0
 - [Finmap library version ≥ 1.5.1](https://github.com/math-comp/finmap)
 - [Hierarchy builder version >= 1.2.0](https://github.com/math-comp/hierarchy-builder)
 
@@ -71,12 +71,12 @@ using [proof general for emacs](https://github.com/ProofGeneral/PG)
 
 ## Break-down of phase 3 of the installation procedure step by step
 
-With the example of Coq 8.14.0 and MathComp 1.13.0. For other versions, update the
+With the example of Coq 8.15.0 and MathComp 1.13.0. For other versions, update the
 version numbers accordingly.
 
-1. Install Coq 8.14.0
+1. Install Coq 8.15.0
 ```
-$ opam install coq.8.14.0
+$ opam install coq.8.15.0
 ```
 2. Install the Mathematical Components
 ```

README.md

@@ -33,7 +33,7 @@ the Coq proof-assistant and using the Mathematical Components library.
   - Pierre-Yves Strub (initial)
   - Laurent Théry
 - License: [CeCILL-C](LICENSE)
-- Compatible Coq versions: Coq 8.14 to 8.18 (or dev)
+- Compatible Coq versions: Coq 8.15 to 8.18 (or dev)
 - Additional dependencies:
   - [MathComp ssreflect 1.13 or later](https://math-comp.github.io)
   - [MathComp fingroup 1.13 or later](https://math-comp.github.io)