packaging for v8.5

18 files changed, 112 insertions, 43 deletions

diff --git a/mathcomp/algebra/cyclic.v b/mathcomp/algebra/cyclic.v
index ad10492..caeb57f 100644
--- a/mathcomp/algebra/cyclic.v
+++ b/mathcomp/algebra/cyclic.v
@@ -1,7 +1,11 @@
 (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
-Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq div fintype bigop.
-Require Import prime finset fingroup morphism perm automorphism quotient.
-Require Import gproduct ssralg finalg zmodp poly.
+(*v8.5 From mathcomp.ssreflect *)
+Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq.
+(*v8.5 From mathcomp.discrete *)
+Require Import div fintype bigop prime finset.
+(*v8.5 From mathcomp.fingroup *)
+Require Import fingroup morphism perm automorphism quotient gproduct.
+Require Import ssralg finalg zmodp poly.
 
 (******************************************************************************)
 (*  Properties of cyclic groups.                                              *)
diff --git a/mathcomp/algebra/finalg.v b/mathcomp/algebra/finalg.v
index b903577..d364fc9 100644
--- a/mathcomp/algebra/finalg.v
+++ b/mathcomp/algebra/finalg.v
@@ -1,6 +1,11 @@
 (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
-Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype.
-Require Import ssralg finset fingroup morphism perm action.
+(*v8.5 From mathcomp.ssreflect *)
+Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq.
+(*v8.5 From mathcomp.discrete *)
+Require Import choice fintype finset.
+(*v8.5 From mathcomp.fingroup *)
+Require Import fingroup morphism perm action.
+Require Import ssralg.
 
 (*****************************************************************************)
 (* This file clones the entire ssralg hierachy for finite types; this allows *)
diff --git a/mathcomp/algebra/fraction.v b/mathcomp/algebra/fraction.v
index 732cc19..446248f 100644
--- a/mathcomp/algebra/fraction.v
+++ b/mathcomp/algebra/fraction.v
@@ -1,6 +1,9 @@
 (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
-Require Import ssreflect ssrfun ssrbool eqtype ssrnat div seq choice tuple.
-Require Import bigop ssralg poly polydiv generic_quotient.
+(*v8.5 From mathcomp.ssreflect *)
+Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq.
+(*v8.5 From mathcomp.discrete *)
+Require Import div choice tuple bigop generic_quotient.
+Require Import ssralg poly polydiv.
 
 (* This file builds the field of fraction of any integral domain. *)
 (* The main result of this file is the existence of the field *)
diff --git a/mathcomp/algebra/intdiv.v b/mathcomp/algebra/intdiv.v
index 4f1ce95..bfd4b13 100644
--- a/mathcomp/algebra/intdiv.v
+++ b/mathcomp/algebra/intdiv.v
@@ -1,7 +1,12 @@
 (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
-Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq path div choice.
-Require Import fintype tuple finfun bigop prime ssralg poly ssrnum ssrint rat.
-Require Import polydiv finalg perm zmodp matrix mxalgebra vector.
+(*v8.5 From mathcomp.ssreflect *)
+Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq.
+(*v8.5 From mathcomp.discrete *)
+Require Import path div choice fintype tuple finfun bigop prime.
+(*v8.5 From mathcomp.fingroup *)
+Require Import perm.
+Require Import ssralg poly ssrnum ssrint rat.
+Require Import polydiv finalg zmodp matrix mxalgebra vector.
 
 (******************************************************************************)
 (* This file provides various results on divisibility of integers.            *)
diff --git a/mathcomp/algebra/interval.v b/mathcomp/algebra/interval.v
index 1f59ce2..7bde270 100644
--- a/mathcomp/algebra/interval.v
+++ b/mathcomp/algebra/interval.v
@@ -1,6 +1,11 @@
 (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
-Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq div choice fintype.
-Require Import bigop ssralg finset fingroup zmodp ssrint ssrnum.
+(*v8.5 From mathcomp.ssreflect *)
+Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq.
+(*v8.5 From mathcomp.discrete *)
+Require Import div choice fintype bigop finset.
+(*v8.5 From mathcomp.fingroup *)
+Require Import fingroup.
+Require Import ssralg zmodp ssrint ssrnum.
 
 (*****************************************************************************)
 (* This file provide support for intervals in numerical and real domains.    *)
diff --git a/mathcomp/algebra/matrix.v b/mathcomp/algebra/matrix.v
index ecf5801..e67008d 100644
--- a/mathcomp/algebra/matrix.v
+++ b/mathcomp/algebra/matrix.v
@@ -1,7 +1,11 @@
 (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
-Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq div choice fintype.
-Require Import finfun bigop prime binomial ssralg finset fingroup finalg.
-Require Import perm zmodp.
+(*v8.5 From mathcomp.ssreflect *)
+Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq.
+(*v8.5 From mathcomp.discrete *)
+Require Import  div choice fintype finfun bigop prime binomial finset.
+(*v8.5 From mathcomp.fingroup *)
+Require Import fingroup perm.
+Require Import ssralg finalg zmodp.
 
 (******************************************************************************)
 (* Basic concrete linear algebra : definition of type for matrices, and all   *)
diff --git a/mathcomp/algebra/mxalgebra.v b/mathcomp/algebra/mxalgebra.v
index 54d5588..833a229 100644
--- a/mathcomp/algebra/mxalgebra.v
+++ b/mathcomp/algebra/mxalgebra.v
@@ -1,7 +1,11 @@
 (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
-Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq div choice fintype.
-Require Import finfun bigop prime binomial ssralg finset fingroup finalg.
-Require Import perm zmodp matrix.
+(*v8.5 From mathcomp.ssreflect *)
+Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq.
+(*v8.5 From mathcomp.discrete *)
+Require Import div choice fintype finfun bigop prime binomial finset.
+(*v8.5 From mathcomp.fingroup *)
+Require Import fingroup perm.
+Require Import ssralg finalg zmodp matrix.
 
 (*****************************************************************************)
 (* In this file we develop the rank and row space theory of matrices, based  *)
diff --git a/mathcomp/algebra/mxpoly.v b/mathcomp/algebra/mxpoly.v
index 7e889a0..8a0b519 100644
--- a/mathcomp/algebra/mxpoly.v
+++ b/mathcomp/algebra/mxpoly.v
@@ -1,7 +1,11 @@
 (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
-Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq div fintype tuple.
-Require Import finfun bigop fingroup perm ssralg zmodp matrix mxalgebra.
-Require Import poly polydiv.
+(*v8.5 From mathcomp.ssreflect *)
+Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq.
+(*v8.5 From mathcomp.discrete *)
+Require Import div fintype tuple finfun bigop.
+(*v8.5 From mathcomp.fingroup *)
+Require Import fingroup perm.
+Require Import ssralg zmodp matrix mxalgebra poly polydiv.
 
 (******************************************************************************)
 (*   This file provides basic support for formal computation with matrices,   *)
diff --git a/mathcomp/algebra/poly.v b/mathcomp/algebra/poly.v
index 813f70d..e473f2d 100644
--- a/mathcomp/algebra/poly.v
+++ b/mathcomp/algebra/poly.v
@@ -1,6 +1,10 @@
 (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
-Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq div choice fintype.
-Require Import bigop ssralg binomial.
+(*v8.5 From mathcomp.ssreflect *)
+Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq.
+(*v8.5 From mathcomp.discrete *)
+Require Import div choice fintype bigop binomial.
+Require Import ssralg.
+
 
 (******************************************************************************)
 (* This file provides a library for univariate polynomials over ring          *)
diff --git a/mathcomp/algebra/polyXY.v b/mathcomp/algebra/polyXY.v
index 3d2292e..5abc40d 100644
--- a/mathcomp/algebra/polyXY.v
+++ b/mathcomp/algebra/polyXY.v
@@ -1,7 +1,11 @@
 (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
-Require Import ssreflect ssrfun ssrbool choice eqtype ssrnat seq div fintype.
-Require Import tuple finfun bigop fingroup perm ssralg zmodp matrix mxalgebra.
-Require Import poly polydiv mxpoly binomial.
+(*v8.5 From mathcomp.ssreflect *)
+Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq.
+(*v8.5 From mathcomp.discrete *)
+Require Import choice div fintype tuple finfun bigop binomial.
+(*v8.5 From mathcomp.fingroup *)
+Require Import fingroup perm.
+Require Import ssralg zmodp matrix mxalgebra poly polydiv mxpoly.
 
 (******************************************************************************)
 (* This file provides additional primitives and theory for bivariate          *)
diff --git a/mathcomp/algebra/polydiv.v b/mathcomp/algebra/polydiv.v
index eca9a27..fa3a132 100644
--- a/mathcomp/algebra/polydiv.v
+++ b/mathcomp/algebra/polydiv.v
@@ -1,6 +1,9 @@
 (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
-Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype.
-Require Import bigop ssralg poly.
+(*v8.5 From mathcomp.ssreflect *)
+Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq.
+(*v8.5 From mathcomp.discrete *)
+Require Import bigop choice fintype.
+Require Import ssralg poly.
 
 (******************************************************************************)
 (* This file provides a library for the basic theory of Euclidean and pseudo- *)
diff --git a/mathcomp/algebra/rat.v b/mathcomp/algebra/rat.v
index b2b88d9..342eead 100644
--- a/mathcomp/algebra/rat.v
+++ b/mathcomp/algebra/rat.v
@@ -1,6 +1,9 @@
 (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
-Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype.
-Require Import bigop ssralg div ssrnum ssrint.
+(*v8.5 From mathcomp.ssreflect *)
+Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq.
+(*v8.5 From mathcomp.discrete *)
+Require Import div choice fintype bigop.
+Require Import ssralg ssrnum ssrint.
 
 (******************************************************************************)
 (* This file defines a datatype for rational numbers and equips it with a     *)
diff --git a/mathcomp/algebra/ring_quotient.v b/mathcomp/algebra/ring_quotient.v
index 479508c..6f2a2f5 100644
--- a/mathcomp/algebra/ring_quotient.v
+++ b/mathcomp/algebra/ring_quotient.v
@@ -1,7 +1,9 @@
 (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
-Require Import eqtype choice ssreflect ssrbool ssrnat ssrfun seq.
-Require Import ssralg generic_quotient.
-
+(*v8.5 From mathcomp.ssreflect *)
+Require Import ssreflect ssrfun ssrbool ssrnat eqtype seq.
+(*v8.5 From mathcomp.discrete *)
+Require Import choice generic_quotient.
+Require Import ssralg.
 
 (******************************************************************************)
 (*          This file describes quotients of algebraic structures.            *)
diff --git a/mathcomp/algebra/ssralg.v b/mathcomp/algebra/ssralg.v
index 5f4592b..3627447 100644
--- a/mathcomp/algebra/ssralg.v
+++ b/mathcomp/algebra/ssralg.v
@@ -1,6 +1,8 @@
 (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
-Require Import ssreflect ssrfun ssrbool eqtype ssrnat div seq choice fintype.
-Require Import finfun bigop prime binomial.
+(*v8.5 From mathcomp.ssreflect *)
+Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq.
+(*v8.5 From mathcomp.discrete *)
+Require Import div choice fintype finfun bigop prime binomial.
 
 (******************************************************************************)
 (*   The algebraic part of the Algebraic Hierarchy, as described in           *)
diff --git a/mathcomp/algebra/ssrint.v b/mathcomp/algebra/ssrint.v
index cbf726e..3281c44 100644
--- a/mathcomp/algebra/ssrint.v
+++ b/mathcomp/algebra/ssrint.v
@@ -1,6 +1,10 @@
 (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
-Require Import ssreflect ssrfun ssrbool eqtype ssrnat choice seq.
-Require Import fintype finfun bigop ssralg ssrnum poly.
+(*v8.5 From mathcomp.ssreflect *)
+Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq.
+(*v8.5 From mathcomp.discrete *)
+Require Import choice fintype finfun bigop.
+Require Import ssralg ssrnum poly.
+
 Import GRing.Theory Num.Theory.
 
 (******************************************************************************)
diff --git a/mathcomp/algebra/ssrnum.v b/mathcomp/algebra/ssrnum.v
index ab7afd0..19d4c31 100644
--- a/mathcomp/algebra/ssrnum.v
+++ b/mathcomp/algebra/ssrnum.v
@@ -1,6 +1,11 @@
 (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
-Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq div choice fintype.
-Require Import bigop ssralg finset fingroup zmodp poly.
+(*v8.5 From mathcomp.ssreflect *)
+Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq.
+(*v8.5 From mathcomp.discrete *)
+Require Import div choice fintype bigop finset.
+(*v8.5 From mathcomp.fingroup *)
+Require Import fingroup.
+Require Import ssralg zmodp poly.
 
 (******************************************************************************)
 (*                                                                            *)
diff --git a/mathcomp/algebra/vector.v b/mathcomp/algebra/vector.v
index 2cb59e9..0d4ace0 100644
--- a/mathcomp/algebra/vector.v
+++ b/mathcomp/algebra/vector.v
@@ -1,6 +1,9 @@
 (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
-Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype bigop.
-Require Import finfun tuple ssralg matrix mxalgebra zmodp.
+(*v8.5 From mathcomp.ssreflect *)
+Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq.
+(*v8.5 From mathcomp.discrete *)
+Require Import choice fintype bigop finfun tuple.
+Require Import ssralg matrix mxalgebra zmodp.
 
 (******************************************************************************)
 (*  * Finite dimensional vector spaces                                        *)
diff --git a/mathcomp/algebra/zmodp.v b/mathcomp/algebra/zmodp.v
index df5b378..614bf10 100644
--- a/mathcomp/algebra/zmodp.v
+++ b/mathcomp/algebra/zmodp.v
@@ -1,6 +1,11 @@
 (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
-Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq div.
-Require Import fintype bigop finset prime fingroup ssralg finalg.
+(*v8.5 From mathcomp.ssreflect *)
+Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq.
+(*v8.5 From mathcomp.discrete *)
+Require Import  div fintype bigop finset prime.
+(*v8.5 From mathcomp.fingroup *)
+Require Import fingroup.
+Require Import ssralg finalg.
 
 (******************************************************************************)
 (*  Definition of the additive group and ring Zp, represented as 'I_p         *)