adapting solvable to 8.5

18 files changed, 170 insertions, 53 deletions

diff --git a/mathcomp/solvable/abelian.v b/mathcomp/solvable/abelian.v
index 8c412dc..52f92ec 100644
--- a/mathcomp/solvable/abelian.v
+++ b/mathcomp/solvable/abelian.v
@@ -1,8 +1,14 @@
 (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
-Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq path div fintype.
-Require Import finfun bigop finset prime binomial fingroup morphism perm.
-Require Import automorphism action quotient gfunctor gproduct zmodp cyclic.
-Require Import pgroup gseries nilpotent sylow.
+Require Import mathcomp.ssreflect.ssreflect.
+From mathcomp.ssreflect
+Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq.
+From mathcomp.discrete
+Require Import path div fintype finfun bigop finset prime binomial.
+From mathcomp.fingroup
+Require Import fingroup morphism perm automorphism action quotient gproduct.
+From mathcomp.algebra
+Require Import cyclic zmodp.
+Require Import gfunctor pgroup gseries nilpotent sylow.
 
 (******************************************************************************)
 (* Constructions based on abelian groups and their structure, with some       *)
diff --git a/mathcomp/solvable/alt.v b/mathcomp/solvable/alt.v
index 3f12ad7..3ee2526 100644
--- a/mathcomp/solvable/alt.v
+++ b/mathcomp/solvable/alt.v
@@ -1,7 +1,14 @@
 (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
-Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq div fintype tuple.
-Require Import tuple bigop prime finset fingroup morphism perm automorphism.
-Require Import quotient action cyclic pgroup gseries sylow primitive_action.
+Require Import mathcomp.ssreflect.ssreflect.
+From mathcomp.ssreflect
+Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq.
+From mathcomp.discrete
+Require Import div fintype tuple finfun bigop prime finset.
+From mathcomp.fingroup
+Require Import fingroup morphism perm automorphism quotient action.
+From mathcomp.algebra
+Require Import cyclic.
+Require Import pgroup gseries sylow primitive_action.
 
 (******************************************************************************)
 (*  Definitions of the symmetric and alternate groups, and some properties.   *)
diff --git a/mathcomp/solvable/burnside_app.v b/mathcomp/solvable/burnside_app.v
index 8fe0b3f..635fd84 100644
--- a/mathcomp/solvable/burnside_app.v
+++ b/mathcomp/solvable/burnside_app.v
@@ -1,6 +1,12 @@
 (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
-Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq div choice fintype.
-Require Import tuple finfun bigop finset fingroup action perm primitive_action.
+Require Import mathcomp.ssreflect.ssreflect.
+From mathcomp.ssreflect
+Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq.
+From mathcomp.discrete
+Require Import div choice fintype tuple finfun bigop finset.
+From mathcomp.fingroup
+Require Import fingroup action perm.
+Require Import primitive_action.
 
 (*   Application of the Burside formula to count the number of distinct       *)
 (* colorings of the vertices of a square and a cube.                          *)
diff --git a/mathcomp/solvable/center.v b/mathcomp/solvable/center.v
index 0ed9200..6226861 100644
--- a/mathcomp/solvable/center.v
+++ b/mathcomp/solvable/center.v
@@ -1,7 +1,14 @@
 (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
-Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq div fintype bigop.
-Require Import finset fingroup morphism perm automorphism quotient action.
-Require Import gproduct gfunctor cyclic.
+Require Import mathcomp.ssreflect.ssreflect.
+From mathcomp.ssreflect
+Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq.
+From mathcomp.discrete
+Require Import path div fintype bigop finset.
+From mathcomp.fingroup
+Require Import fingroup morphism perm automorphism quotient action gproduct.
+From mathcomp.algebra
+Require Import cyclic.
+Require Import gfunctor.
 
 (******************************************************************************)
 (* Definition of the center of a group and of external central products:      *)
diff --git a/mathcomp/solvable/commutator.v b/mathcomp/solvable/commutator.v
index 81be11d..6f6a2b5 100644
--- a/mathcomp/solvable/commutator.v
+++ b/mathcomp/solvable/commutator.v
@@ -1,6 +1,12 @@
 (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
-Require Import ssreflect ssrfun ssrbool eqtype ssrnat fintype bigop finset.
-Require Import binomial fingroup morphism automorphism quotient gfunctor.
+Require Import mathcomp.ssreflect.ssreflect.
+From mathcomp.ssreflect
+Require Import ssreflect ssrbool ssrfun eqtype ssrnat.
+From mathcomp.discrete
+Require Import fintype bigop finset prime binomial.
+From mathcomp.fingroup
+Require Import fingroup morphism automorphism quotient.
+Require Import gfunctor.
 
 (******************************************************************************)
 (*   This files contains the proofs of several key properties of commutators, *)
diff --git a/mathcomp/solvable/extraspecial.v b/mathcomp/solvable/extraspecial.v
index c38d17a..737838b 100644
--- a/mathcomp/solvable/extraspecial.v
+++ b/mathcomp/solvable/extraspecial.v
@@ -1,9 +1,17 @@
 (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
-Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq div choice fintype.
-Require Import bigop finset prime binomial fingroup morphism perm automorphism.
-Require Import presentation quotient action commutator gproduct gfunctor.
-Require Import ssralg finalg zmodp cyclic pgroup center gseries.
-Require Import nilpotent sylow abelian finmodule matrix maximal extremal.
+Require Import mathcomp.ssreflect.ssreflect.
+From mathcomp.ssreflect
+Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq.
+From mathcomp.discrete
+Require Import path div choice fintype bigop finset prime binomial.
+From mathcomp.fingroup
+Require Import fingroup morphism perm automorphism quotient action gproduct.
+From mathcomp.fingroup
+Require Import presentation.
+From mathcomp.algebra
+Require Import ssralg finalg zmodp matrix cyclic.
+Require Import pgroup center gseries commutator gfunctor.
+Require Import nilpotent sylow abelian finmodule maximal extremal.
 
 (******************************************************************************)
 (* This file contains the fine structure thorems for extraspecial p-groups.   *)
diff --git a/mathcomp/solvable/extremal.v b/mathcomp/solvable/extremal.v
index b8cb69d..e233a86 100644
--- a/mathcomp/solvable/extremal.v
+++ b/mathcomp/solvable/extremal.v
@@ -1,9 +1,17 @@
 (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
-Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq div choice fintype.
-Require Import bigop finset prime binomial fingroup morphism perm automorphism.
-Require Import presentation quotient action commutator gproduct gfunctor.
-Require Import ssralg finalg zmodp cyclic pgroup center gseries.
-Require Import nilpotent sylow abelian finmodule matrix maximal.
+Require Import mathcomp.ssreflect.ssreflect.
+From mathcomp.ssreflect
+Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq.
+From mathcomp.discrete
+Require Import path div choice fintype bigop finset prime binomial.
+From mathcomp.fingroup
+Require Import fingroup morphism perm automorphism quotient action gproduct.
+From mathcomp.fingroup
+Require Import presentation.
+From mathcomp.algebra
+Require Import ssralg finalg zmodp cyclic matrix.
+Require Import pgroup center gseries commutator gfunctor.
+Require Import nilpotent sylow abelian finmodule maximal.
 
 (******************************************************************************)
 (*    This file contains the definition and properties of extremal p-groups;  *)
diff --git a/mathcomp/solvable/finmodule.v b/mathcomp/solvable/finmodule.v
index e2eae84..dd84def 100644
--- a/mathcomp/solvable/finmodule.v
+++ b/mathcomp/solvable/finmodule.v
@@ -1,7 +1,14 @@
 (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
-Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq path div choice.
-Require Import fintype bigop ssralg finset fingroup morphism perm.
-Require Import finalg action gproduct commutator cyclic.
+Require Import mathcomp.ssreflect.ssreflect.
+From mathcomp.ssreflect
+Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq.
+From mathcomp.discrete
+Require Import path div choice fintype bigop prime finset.
+From mathcomp.fingroup
+Require Import fingroup morphism perm action gproduct.
+From mathcomp.algebra
+Require Import ssralg finalg cyclic.
+Require Import commutator.
 
 (******************************************************************************)
 (*  This file regroups constructions and results that are based on the most   *)
diff --git a/mathcomp/solvable/frobenius.v b/mathcomp/solvable/frobenius.v
index 492c802..64fe7e6 100644
--- a/mathcomp/solvable/frobenius.v
+++ b/mathcomp/solvable/frobenius.v
@@ -1,7 +1,14 @@
 (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
-Require Import ssreflect ssrfun ssrbool eqtype ssrnat div fintype bigop prime.
-Require Import finset fingroup morphism perm action quotient gproduct.
-Require Import cyclic center pgroup nilpotent sylow hall abelian.
+Require Import mathcomp.ssreflect.ssreflect.
+From mathcomp.ssreflect
+Require Import ssreflect ssrbool ssrfun eqtype ssrnat.
+From mathcomp.discrete
+Require Import div fintype bigop prime finset.
+From mathcomp.fingroup
+Require Import fingroup morphism perm action quotient gproduct.
+From mathcomp.algebra
+Require Import cyclic.
+Require Import center pgroup nilpotent sylow hall abelian.
 
 (******************************************************************************)
 (*  Definition of Frobenius groups, some basic results, and the Frobenius     *)
diff --git a/mathcomp/solvable/gfunctor.v b/mathcomp/solvable/gfunctor.v
index a338999..25295ff 100644
--- a/mathcomp/solvable/gfunctor.v
+++ b/mathcomp/solvable/gfunctor.v
@@ -1,5 +1,10 @@
 (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
-Require Import ssreflect ssrbool ssrfun eqtype ssrnat fintype bigop finset.
+Require Import mathcomp.ssreflect.ssreflect.
+From mathcomp.ssreflect
+Require Import ssreflect ssrbool ssrfun eqtype ssrnat.
+From mathcomp.discrete
+Require Import fintype bigop finset.
+From mathcomp.fingroup
 Require Import fingroup morphism automorphism quotient gproduct.
 
 (******************************************************************************)
diff --git a/mathcomp/solvable/gseries.v b/mathcomp/solvable/gseries.v
index 4e299e3..718f074 100644
--- a/mathcomp/solvable/gseries.v
+++ b/mathcomp/solvable/gseries.v
@@ -1,7 +1,13 @@
 (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
-Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq path fintype bigop.
-Require Import finset fingroup morphism automorphism quotient action.
+Require Import mathcomp.ssreflect.ssreflect.
+From mathcomp.ssreflect
+Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq.
+From mathcomp.discrete
+Require Import path div choice fintype bigop finset.
+From mathcomp.fingroup
+Require Import fingroup morphism automorphism quotient action.
 Require Import commutator center.
+
 (******************************************************************************)
 (*           H <|<| G   <=> H is subnormal in G, i.e., H <| ... <| G.         *)
 (* invariant_factor A H G <=> A normalises both H and G, and H <| G.          *)
diff --git a/mathcomp/solvable/hall.v b/mathcomp/solvable/hall.v
index e097765..90ba407 100644
--- a/mathcomp/solvable/hall.v
+++ b/mathcomp/solvable/hall.v
@@ -1,6 +1,11 @@
 (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
-Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq div fintype finset.
-Require Import prime fingroup morphism automorphism quotient action gproduct.
+Require Import mathcomp.ssreflect.ssreflect.
+From mathcomp.ssreflect
+Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq.
+From mathcomp.discrete
+Require Import path div choice fintype finset bigop prime.
+From mathcomp.fingroup
+Require Import fingroup morphism automorphism quotient action gproduct.
 Require Import commutator center pgroup finmodule nilpotent sylow.
 Require Import abelian maximal.
 
diff --git a/mathcomp/solvable/jordanholder.v b/mathcomp/solvable/jordanholder.v
index bc7bec2..82d9c8b 100644
--- a/mathcomp/solvable/jordanholder.v
+++ b/mathcomp/solvable/jordanholder.v
@@ -1,6 +1,11 @@
 (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
-Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq path choice fintype.
-Require Import bigop finset fingroup morphism automorphism quotient action.
+Require Import mathcomp.ssreflect.ssreflect.
+From mathcomp.ssreflect
+Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq.
+From mathcomp.discrete
+Require Import path div choice fintype tuple finfun bigop finset.
+From mathcomp.fingroup
+Require Import fingroup morphism automorphism quotient action.
 Require Import gseries.
 
 (******************************************************************************)
diff --git a/mathcomp/solvable/maximal.v b/mathcomp/solvable/maximal.v
index 7b50dc9..a3cd11c 100644
--- a/mathcomp/solvable/maximal.v
+++ b/mathcomp/solvable/maximal.v
@@ -1,8 +1,14 @@
 (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
-Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq choice div fintype.
-Require Import finfun bigop finset prime binomial fingroup morphism perm.
-Require Import automorphism quotient action commutator gproduct gfunctor.
-Require Import ssralg finalg zmodp cyclic pgroup center gseries.
+Require Import mathcomp.ssreflect.ssreflect.
+From mathcomp.ssreflect
+Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq.
+From mathcomp.discrete
+Require Import div choice fintype finfun bigop finset prime binomial.
+From mathcomp.fingroup
+Require Import fingroup morphism perm automorphism quotient action gproduct.
+From mathcomp.algebra
+Require Import ssralg finalg zmodp cyclic.
+Require Import pgroup center gseries commutator gfunctor.
 Require Import nilpotent sylow abelian finmodule.
 
 (******************************************************************************)
diff --git a/mathcomp/solvable/nilpotent.v b/mathcomp/solvable/nilpotent.v
index 5b271de..e1baa3f 100644
--- a/mathcomp/solvable/nilpotent.v
+++ b/mathcomp/solvable/nilpotent.v
@@ -1,7 +1,14 @@
 (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
-Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq path fintype div.
-Require Import bigop prime finset fingroup morphism automorphism quotient.
-Require Import commutator gproduct gfunctor center gseries cyclic.
+Require Import mathcomp.ssreflect.ssreflect.
+From mathcomp.ssreflect
+Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq.
+From mathcomp.discrete
+Require Import path fintype div bigop prime finset.
+From mathcomp.fingroup
+Require Import fingroup morphism automorphism quotient gproduct.
+From mathcomp.algebra
+Require Import cyclic.
+Require Import commutator gfunctor center gseries.
 
 (******************************************************************************)
 (*   This file defines nilpotent and solvable groups, and give some of their  *)
diff --git a/mathcomp/solvable/pgroup.v b/mathcomp/solvable/pgroup.v
index c6db976..b1d2bf6 100644
--- a/mathcomp/solvable/pgroup.v
+++ b/mathcomp/solvable/pgroup.v
@@ -1,7 +1,14 @@
 (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
-Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq div.
-Require Import fintype bigop finset prime fingroup morphism.
-Require Import gfunctor automorphism quotient action gproduct cyclic.
+Require Import mathcomp.ssreflect.ssreflect.
+From mathcomp.ssreflect
+Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq.
+From mathcomp.discrete
+Require Import div fintype bigop finset prime.
+From mathcomp.fingroup
+Require Import fingroup morphism automorphism quotient action gproduct.
+From mathcomp.algebra
+Require Import cyclic.
+Require Import gfunctor.
 
 (******************************************************************************)
 (* Standard group notions and constructions based on the prime decomposition  *)
diff --git a/mathcomp/solvable/primitive_action.v b/mathcomp/solvable/primitive_action.v
index 7e2075d..06ab30e 100644
--- a/mathcomp/solvable/primitive_action.v
+++ b/mathcomp/solvable/primitive_action.v
@@ -1,7 +1,12 @@
 (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
-Require Import ssreflect ssrbool ssrfun eqtype ssrnat.
-Require Import div seq fintype tuple finset.
-Require Import fingroup action gseries.
+Require Import mathcomp.ssreflect.ssreflect.
+From mathcomp.ssreflect
+Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq.
+From mathcomp.discrete
+Require Import div fintype tuple finset.
+From mathcomp.fingroup
+Require Import fingroup action.
+Require Import gseries.
 
 (******************************************************************************)
 (* n-transitive and primitive actions:                                        *)
diff --git a/mathcomp/solvable/sylow.v b/mathcomp/solvable/sylow.v
index 02ab37a..abaa2a5 100644
--- a/mathcomp/solvable/sylow.v
+++ b/mathcomp/solvable/sylow.v
@@ -1,7 +1,16 @@
 (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
-Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq div fintype prime.
-Require Import bigop finset fingroup morphism automorphism quotient action.
-Require Import cyclic gproduct commutator pgroup center nilpotent.
+Require Import mathcomp.ssreflect.ssreflect.
+From mathcomp.ssreflect
+Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq.
+From mathcomp.discrete
+Require Import div fintype finset bigop prime.
+From mathcomp.fingroup
+Require Import fingroup morphism automorphism quotient action gproduct.
+From mathcomp.algebra
+Require Import ssralg poly ssrnum ssrint rat.
+From mathcomp.algebra
+Require Import polydiv finalg zmodp matrix mxalgebra vector cyclic.
+Require Import commutator pgroup center nilpotent.
 
 (******************************************************************************)
 (*   The Sylow theorem and its consequences, including the Frattini argument, *)