Update to MathComp 2.5

Author: hivert

Makefile

@@ -7,7 +7,7 @@
 ##         #     GNU Lesser General Public License Version 2.1          ##
 ##         #     (see LICENSE file for the text of the license)         ##
 ##########################################################################
-## GNUMakefile for Rocq 9.0.0
+## GNUMakefile for Rocq 9.0.1
 
 # For debugging purposes (must stay here, don't move below)
 INITIAL_VARS := $(.VARIABLES)
@@ -278,7 +278,7 @@ COQDOCLIBS?=$(COQLIBS_NOML)
 # generated this makefile
 # NB --print-version is not in the rocq shim
 COQ_VERSION:=$(shell $(ROCQ) c --print-version | cut -d " " -f 1)
-COQMAKEFILE_VERSION:=9.0.0
+COQMAKEFILE_VERSION:=9.0.1
 
 # COQ_SRC_SUBDIRS is for user-overriding, usually to add
 # `user-contrib/Foo` to the includes, we keep COQCORE_SRC_SUBDIRS for
@@ -682,8 +682,8 @@ clean::
 	$(HIDE)rm -f $(VOFILES)
 	$(HIDE)rm -f $(VOFILES:.vo=.vos)
 	$(HIDE)rm -f $(VOFILES:.vo=.vok)
-	$(HIDE)rm -f $(VOFILES:.vo=.v.prof.json)
-	$(HIDE)rm -f $(VOFILES:.vo=.v.prof.json.gz)
+	$(HIDE)rm -f $(VOFILES:.vo=.vo.prof.json)
+	$(HIDE)rm -f $(VOFILES:.vo=.vo.prof.json.gz)
 	$(HIDE)rm -f $(BEAUTYFILES) $(VFILES:=.old)
 	$(HIDE)rm -f all.ps all-gal.ps all.pdf all-gal.pdf all.glob all-mli.tex
 	$(HIDE)rm -f $(VFILES:.v=.glob)

README.md

@@ -168,20 +168,22 @@ Installation
 This library is based on
 
 * [SSReflect/MathComp 2](https://github.com/math-comp/math-comp)
-  Library version 2.4.0 or more recent.
-* This branch is *not* compatible with version MathComp 2.3.0.
+  Library version 2.5.0 or more recent.
+* This branch is *not* compatible with version MathComp 2.4.0.
+
+* For MathComp 2.4.0, use the [MathComp-2.4.0](https://github.com/math-comp/Coq-Combi/tree/MathComp-2.4.0) branch.
 
 * For MathComp 2.3.0, use the [MathComp-2.3.0](https://github.com/math-comp/Coq-Combi/tree/MathComp-2.3.0) branch.
 
 * For MathComp 2.2.0, use the [MathComp-2.2.0](https://github.com/math-comp/Coq-Combi/tree/MathComp-2.2.0) branch.
 
 Here are the Opam packages I'm using
 ```
-coq-hierarchy-builder        1.9.0
-coq-mathcomp-ssreflect       2.4.0
-coq-mathcomp-algebra         2.4.0
-coq-mathcomp-field           2.4.0
-coq-mathcomp-fingroup        2.4.0
-coq-mathcomp-character       2.4.0
-coq-mathcomp-multinomials    2.4.0
+coq-hierarchy-builder        1.9.1
+coq-mathcomp-ssreflect       2.5.0
+coq-mathcomp-algebra         2.5.0
+coq-mathcomp-field           2.5.0
+coq-mathcomp-fingroup        2.5.0
+coq-mathcomp-character       2.5.0
+coq-mathcomp-multinomials    2.5.0
 ```

theories/Basic/combclass.v

@@ -22,7 +22,7 @@ ways, three from a list (see [sub_subFinType], [sub_uniq_subFinType] and
 constructed subfintypes (see [union_subFinType] below).  *)
 
 From HB Require Import structures.
-From mathcomp Require Import all_ssreflect.
+From mathcomp Require Import all_boot.
 Require Import tools.
 
 Set Implicit Arguments.

theories/Basic/congr.v

@@ -68,7 +68,7 @@ the congruence transitive closure of rule. The main results here are
                    preserved along the rewriting rule holds for classes.      *)
 (******************************************************************************)
 From HB Require Import structures.
-From mathcomp Require Import all_ssreflect.
+From mathcomp Require Import all_boot.
 From Stdlib Require Import Recdef.
 Require Import permcomp permuted multinomial vectNK.
 

theories/Basic/ordtype.v

@@ -40,7 +40,7 @@ Cover relation:
                   [finPOrderType].
  ********)
 From HB Require Import structures.
-From mathcomp Require Import all_ssreflect.
+From mathcomp Require Import all_boot.
 From mathcomp Require Import order.
 Require Import tools.
 

theories/Basic/unitriginv.v

@@ -30,8 +30,7 @@ therefore invertible. Moreover Lemma [Minv_unitrig] says that the inverse
 is unitriangular too.
  *******)
 From Corelib Require Import Setoid.
-Require Import mathcomp.ssreflect.ssreflect.
-From mathcomp Require Import ssrfun ssrbool eqtype ssrnat order.
+From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat order.
 From mathcomp Require Import fintype bigop ssralg.
 From mathcomp Require Import finset fingroup perm matrix.
 

theories/Combi/Dyckword.v

@@ -67,7 +67,7 @@ rotation trick: there is a (n+1) to 1 map from balanced words to Dyck words.
        have the same cardinality n+1.
  *********************)
 From HB Require Import structures.
-From mathcomp Require Import all_ssreflect.
+From mathcomp Require Import all_boot order.
 From mathcomp Require Import div ssralg ssrint ssrnum binomial.
 Require Import tools combclass bintree.
 
@@ -730,7 +730,7 @@ apply/Dyck_wordP; rewrite height_take_leq; split => [n|].
     rewrite height_simpl take_takel; last exact: ltnW.
     move: Hbal1; rewrite -{1}(cat_take_drop pfminh w) height_simpl => /eqP.
     rewrite -subr_eq0 opprK [height _ + _]addrC -addrA addr_eq0 => /eqP ->.
-    rewrite addrC subr_ge0 lezD1.
+    rewrite [- _ + _]addrC subr_ge0 lezD1.
     by rewrite pfminhP pfminh_min.
 - have : height (rot pfminh w) = -1.
     by rewrite /rot height_cat addrC -height_cat cat_take_drop.

theories/Combi/Yamanouchi.v

@@ -51,7 +51,7 @@ Sigma types for Yamanouchi words:
 
 ******)
 From HB Require Import structures.
-From mathcomp Require Import all_ssreflect.
+From mathcomp Require Import all_boot.
 Require Import tools combclass partition.
 
 Set Implicit Arguments.

theories/Combi/bintree.v

@@ -81,7 +81,7 @@ Tamari Lattice:
 - [t1 /\T t2] == the join of [t1] and [t2] in the Tamari lattice.
  *********************)
 From HB Require Import structures.
-From mathcomp Require Import all_ssreflect.
+From mathcomp Require Import all_boot order.
 Require Import tools combclass ordtype.
 
 Set Implicit Arguments.

theories/Combi/composition.v

@@ -48,7 +48,7 @@ Compositions and partitions:
                    [c : intcompn n]
 ******)
 From HB Require Import structures.
-From mathcomp Require Import all_ssreflect.
+From mathcomp Require Import all_boot order.
 Require Import tools combclass sorted partition subseq ordtype.
 
 Set Implicit Arguments.