Adapt to https://github.com/math-comp/math-comp/pull/1354

.nix/config.nix

@@ -48,10 +48,6 @@ in
   ## alternative configuration
   ## When generating GitHub Action CI, one workflow file
   ## will be created per bundle
-  bundles."8.19".coqPackages = common-bundle // {
-    coq.override.version = "8.19";
-    mathcomp.override.version = "2.2.0";
-  };
 
   bundles."8.20".coqPackages = common-bundle // {
     coq.override.version = "8.20";

INSTALL.md

@@ -2,9 +2,9 @@
 
 ## Requirements
 
-- [The Coq Proof Assistant version ≥ 8.19](https://coq.inria.fr)
-- [Mathematical Components version ≥ 2.1.0](https://github.com/math-comp/math-comp)
-- [Finmap library version ≥ 2.0.0](https://github.com/math-comp/finmap)
+- [The Coq Proof Assistant version ≥ 8.20](https://coq.inria.fr)
+- [Mathematical Components version ≥ 2.2.0](https://github.com/math-comp/math-comp)
+- [Finmap library version ≥ 2.1.0](https://github.com/math-comp/finmap)
 - [Hierarchy builder version >= 1.7.0](https://github.com/math-comp/hierarchy-builder)
 - [bigenough >= 1.0.0](https://github.com/math-comp/bigenough)
 
@@ -71,28 +71,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.19.0 and MathComp 2.1.0. For other versions, update the
+With the example of Coq 8.20.0 and MathComp 2.3.0. For other versions, update the
 version numbers accordingly.
 
-1. Install Coq 8.19.0
+1. Install Coq 8.20.1
 ```
-$ opam install coq.8.19.0
+$ opam install coq.8.20.1
 ```
 2. Install the Mathematical Components
 ```
-$ opam install coq-mathcomp-ssreflect.2.1.0
-$ opam install coq-mathcomp-fingroup.2.1.0
-$ opam install coq-mathcomp-algebra.2.1.0
-$ opam install coq-mathcomp-solvable.2.1.0
-$ opam install coq-mathcomp-field.2.1.0
+$ opam install coq-mathcomp-ssreflect.2.3.0
+$ opam install coq-mathcomp-fingroup.2.3.0
+$ opam install coq-mathcomp-algebra.2.3.0
+$ opam install coq-mathcomp-solvable.2.3.0
+$ opam install coq-mathcomp-field.2.3.0
 ```
 3. Install the Finite maps library
 ```
-$ opam install coq-mathcomp-finmap.2.0.0
+$ opam install coq-mathcomp-finmap.2.1.0
 ```
 4. Install the Hierarchy Builder
 ```
-$ opam install coq-hierarchy-builder.1.6.0
+$ opam install coq-hierarchy-builder.1.8.0
 ```
 5. Download and compile `coq-mathcomp-analysis` without installing
 ```

Makefile.coq.local

@@ -1,5 +1,5 @@
 pre-all::
-	if command -v coqc > /dev/null && (coqc --version | grep -q '8.18\|8.19\|8.20') ; then \
+	if command -v coqc > /dev/null && (coqc --version | grep -q '8.20') ; then \
 	  for f in $(shell grep "From Corelib" $$(find . -name "*.v") | cut -d: -f1) ; do \
 	     sed -i.bak 's/From Corelib/From Coq/' $${f} ; \
 	     sed -i.bak 's/PosDef/PArith/' $${f} ; \

README.md

@@ -28,7 +28,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.19 to 8.20, Rocq 9.0 (or dev)
+- Compatible Rocq versions: Coq 8.20, Rocq 9.0 (or dev)
 - Additional dependencies:
   - [MathComp ssreflect 2.1.0 or later](https://math-comp.github.io)
   - [MathComp fingroup 2.1.0 or later](https://math-comp.github.io)

coq-mathcomp-classical.opam

@@ -15,12 +15,12 @@ the Coq proof-assistant and using the Mathematical Components library."""
 build: [make "-C" "classical" "-j%{jobs}%"]
 install: [make "-C" "classical" "install"]
 depends: [
-  ("coq" {>= "8.19" & < "8.21~"}
+  ("coq" {>= "8.20" & < "8.21~"}
   | "rocq-core" { (>= "9.0" & < "9.1~") | (= "dev") })
-  "coq-mathcomp-ssreflect" { (>= "2.1.0") }
+  "coq-mathcomp-ssreflect" { (>= "2.2.0") }
   "coq-mathcomp-fingroup"
   "coq-mathcomp-algebra"
-  "coq-mathcomp-finmap" { (>= "2.0.0") }
+  "coq-mathcomp-finmap" { (>= "2.1.0") }
   "coq-hierarchy-builder" { (>= "1.7.0") }
 ]
 

experimental_reals/Makefile.coq.local

@@ -1,5 +1,5 @@
 pre-all::
-	if command -v coqc > /dev/null && (coqc --version | grep -q '8.18\|8.19\|8.20') ; then \
+	if command -v coqc > /dev/null && (coqc --version | grep -q '8.20') ; then \
 	  for f in $(shell grep "From Corelib" $$(find . -name "*.v") | cut -d: -f1) ; do \
 	     sed -i.bak 's/From Corelib/From Coq/' $${f} ; \
 	     sed -i.bak 's/PosDef/PArith/' $${f} ; \

reals/Makefile.coq.local

@@ -1,5 +1,5 @@
 pre-all::
-	if command -v coqc > /dev/null && (coqc --version | grep -q '8.18\|8.19\|8.20') ; then \
+	if command -v coqc > /dev/null && (coqc --version | grep -q '8.20') ; then \
 	  for f in $(shell grep "From Corelib" $$(find . -name "*.v") | cut -d: -f1) ; do \
 	     sed -i.bak 's/From Corelib/From Coq/' $${f} ; \
 	     sed -i.bak 's/PosDef/PArith/' $${f} ; \

theories/derive.v

@@ -59,8 +59,8 @@ Reserved Notation "''D_' v f" (at level 10, v, f at next level,
   format "''D_' v  f").
 Reserved Notation "''D_' v f c" (at level 10, v, f at next level,
   format "''D_' v  f  c"). (* printing *)
-Reserved Notation "f ^` ()" (at level 8, format "f ^` ()").
-Reserved Notation "f ^` ( n )" (at level 8, format "f ^` ( n )").
+Reserved Notation "f ^` ()" (format "f ^` ()").
+Reserved Notation "f ^` ( n )" (format "f ^` ( n )").
 
 Section Differential.
 Context {K : numDomainType} {V W : normedModType K}.

theories/forms.v

@@ -15,17 +15,15 @@ Unset Printing Implicit Defensive.
 Local Open Scope ring_scope.
 Import GRing.Theory Num.Theory.
 
-Reserved Notation "'[ u , v ]"
-  (at level 2, format "'[hv' ''[' u , '/ '  v ] ']'").
-Reserved Notation "'[ u , v ]_ M"
-         (at level 2, format "'[hv' ''[' u , '/ '  v ]_ M ']'").
-Reserved Notation "'[ u ]_ M" (at level 2, format "''[' u ]_ M").
-Reserved Notation "'[ u ]" (at level 2, format "''[' u ]").
+Reserved Notation "'[ u , v ]" (format "'[hv' ''[' u , '/ '  v ] ']'").
+Reserved Notation "'[ u , v ]_ M" (format "'[hv' ''[' u , '/ '  v ]_ M ']'").
+Reserved Notation "'[ u ]_ M" (format "''[' u ]_ M").
+Reserved Notation "'[ u ]" (format "''[' u ]").
 Reserved Notation "u '``_' i"
-    (at level 3, i at level 2, left associativity, format "u '``_' i").
+  (at level 3, i at level 2, left associativity, format "u '``_' i").
 Reserved Notation "A ^_|_"    (at level 8, format "A ^_|_").
 Reserved Notation "A _|_ B" (at level 69, format "A  _|_  B").
-Reserved Notation "eps_theta .-sesqui" (at level 2, format "eps_theta .-sesqui").
+Reserved Notation "eps_theta .-sesqui" (format "eps_theta .-sesqui").
 
 Notation "u '``_' i" := (u (0 : 'I_1) i) : ring_scope.
 Notation "''e_' i" := (delta_mx 0 i)

theories/topology_theory/topology_structure.v

@@ -77,9 +77,9 @@ From mathcomp Require Export filter.
 (*                                                                            *)
 (******************************************************************************)
 
-Reserved Notation "A °" (at level 1, format "A °").
-Reserved Notation "[ 'locally' P ]" (at level 0, format "[ 'locally'  P ]").
-Reserved Notation "x ^'" (at level 2, format "x ^'").
+Reserved Notation "A °" (format "A °").
+Reserved Notation "[ 'locally' P ]" (format "[ 'locally'  P ]").
+Reserved Notation "x ^'" (format "x ^'").
 
 Set Implicit Arguments.
 Unset Strict Implicit.