Drop support for Coq 8.20

.nix/config.nix

@@ -53,10 +53,14 @@ in {
   ## When generating GitHub Action CI, one workflow file
   ## will be created per bundle
 
-  bundles."8.20-2.4.0".coqPackages = common-bundle // {
-    coq.override.version = "8.20";
-    mathcomp.override.version = "2.4.0";
-    mathcomp-infotheo.job = false;
+  bundles."9.0-2.4.0" = {
+    rocqPackages = {
+      rocq-core.override.version = "9.0";
+    };
+    coqPackages = common-bundle // {
+      coq.override.version = "9.0";
+      mathcomp.override.version = "2.4.0";
+    };
   };
 
   bundles."9.0" = {

INSTALL.md

@@ -2,7 +2,7 @@
 
 ## Requirements
 
-- [The Coq Proof Assistant version ≥ 8.20 / Rocq Prover version ≥ 9.0](https://rocq-prover.org)
+- [The Rocq Prover version ≥ 9.0](https://rocq-prover.org)
 - [Mathematical Components version ≥ 2.4.0](https://github.com/math-comp/math-comp)
 - [Finmap library version ≥ 2.1.0](https://github.com/math-comp/finmap)
 - [Hierarchy builder version ≥ 1.8.0](https://github.com/math-comp/hierarchy-builder)
@@ -73,28 +73,28 @@ 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.20.1 and MathComp 2.4.0. For other versions, update the
+With the example of Coq 9.1.1 and MathComp 2.5.0. For other versions, update the
 version numbers accordingly.
 
-1. Install Coq 8.20.1
+1. Install Rocq 9.1.1
 ```
-$ opam install coq.8.20.1
+$ opam install rocq-core.9.1.1
 ```
 2. Install the Mathematical Components
 ```
-$ opam install coq-mathcomp-ssreflect.2.4.0
-$ opam install coq-mathcomp-fingroup.2.4.0
-$ opam install coq-mathcomp-algebra.2.4.0
-$ opam install coq-mathcomp-solvable.2.4.0
-$ opam install coq-mathcomp-field.2.4.0
+$ opam install rocq-mathcomp-ssreflect.2.5.0
+$ opam install rocq-mathcomp-fingroup.2.5.0
+$ opam install rocq-mathcomp-algebra.2.5.0
+$ opam install rocq-mathcomp-solvable.2.5.0
+$ opam install rocq-mathcomp-field.2.5.0
 ```
 3. Install the Finite maps library
 ```
-$ opam install coq-mathcomp-finmap.2.2.0
+$ opam install rocq-mathcomp-finmap.2.2.0
 ```
 4. Install the Hierarchy Builder
 ```
-$ opam install coq-hierarchy-builder.1.8.0
+$ opam install rocq-hierarchy-builder.1.10.2
 ```
 5. Download and compile `coq-mathcomp-analysis` without installing
 ```

Makefile.common

@@ -123,7 +123,7 @@ html: build $(DOCDIR)/dependency_graph.dot
 	-Q reals_stdlib mathcomp.reals_stdlib \
 	-Q experimental_reals mathcomp.experimental_reals \
 	-Q analysis_stdlib mathcomp.analysis_stdlib \
-	-coqlib https://rocq-prover.org/doc/V8.20.1/stdlib/ \
+	-coqlib https://rocq-prover.org/doc/V9.0.0/stdlib/ \
 	-dependency-graph $(DOCDIR)/dependency_graph.dot \
 	-hierarchy-graph $(DOCDIR)/hierarchy_graph.dot \
         -index-blacklist etc/rocqnavi_index-blacklist \

README.md

@@ -24,7 +24,7 @@ In terms of [opam](https://opam.ocaml.org/doc/Install.html), it comes as the fol
 
 - [Authors](AUTHORS.md)
 - License: [CeCILL-C](LICENSE)
-- Compatible Rocq versions: Coq 8.20, Rocq 9.0 (or dev)
+- Compatible Rocq versions: Rocq 9.0 and 9.1 (or dev)
 - Additional dependencies:
   - [MathComp ssreflect 2.4.0 or later](https://math-comp.github.io)
   - [MathComp fingroup 2.4.0 or later](https://math-comp.github.io)

coq-mathcomp-classical.opam

@@ -15,8 +15,7 @@ the Coq proof-assistant and using the Mathematical Components library."""
 build: [make "-C" "classical" "-j%{jobs}%"]
 install: [make "-C" "classical" "install"]
 depends: [
-  ("coq" {>= "8.20" & < "8.21~"}
-  | "coq-core" { (>= "9.0" & < "9.2~") | (= "dev") })
+  "coq-core" { (>= "9.0" & < "9.2~") | (= "dev") }
   "coq-mathcomp-ssreflect" { (>= "2.4.0" & < "2.6~") | (= "dev") }
   "coq-mathcomp-fingroup"
   "coq-mathcomp-algebra"