8 files changed, 115 insertions, 40 deletions
diff --git a/mathcomp/character/character.v b/mathcomp/character/character.v
index ac2f491..166fcc5 100644
--- a/mathcomp/character/character.v
+++ b/mathcomp/character/character.v
@@ -1,10 +1,20 @@
 (* (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 finset gproduct.
-Require Import fingroup morphism perm automorphism quotient finalg action.
-Require Import zmodp commutator cyclic center pgroup nilpotent sylow abelian.
-Require Import matrix mxalgebra mxpoly mxrepresentation vector ssrnum algC.
-Require Import classfun.
+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 prime finset.
+From mathcomp.fingroup
+Require Import fingroup morphism perm automorphism quotient action gproduct.
+From mathcomp.algebra
+Require Import ssralg poly finalg zmodp cyclic.
+From mathcomp.algebra
+Require Import matrix mxalgebra mxpoly vector ssrnum.
+From mathcomp.solvable
+Require Import commutator center pgroup nilpotent sylow abelian.
+From mathcomp.field
+Require Import algC.
+Require Import mxrepresentation classfun.
 
 Set Implicit Arguments.
 Unset Strict Implicit.
diff --git a/mathcomp/character/classfun.v b/mathcomp/character/classfun.v
index 16d044b..32eeabb 100644
--- a/mathcomp/character/classfun.v
+++ b/mathcomp/character/classfun.v
@@ -1,9 +1,17 @@
 (* (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 finset.
-Require Import fingroup morphism perm automorphism quotient finalg action.
-Require Import gproduct zmodp commutator cyclic center pgroup sylow.
-Require Import matrix vector falgebra ssrnum algC algnum.
+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 prime finset.
+From mathcomp.fingroup
+Require Import fingroup morphism perm automorphism quotient action gproduct.
+From mathcomp.algebra
+Require Import ssralg poly finalg zmodp cyclic vector ssrnum matrix vector.
+From mathcomp.solvable
+Require Import commutator center pgroup sylow.
+From mathcomp.field
+Require Import falgebra algC algnum.
 
 (******************************************************************************)
 (* This file contains the basic theory of class functions:                    *)
diff --git a/mathcomp/character/finfield.v b/mathcomp/character/finfield.v
index 14a02ef..05b4a31 100644
--- a/mathcomp/character/finfield.v
+++ b/mathcomp/character/finfield.v
@@ -1,9 +1,23 @@
 (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
-Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype div.
-Require Import tuple bigop prime finset fingroup ssralg poly polydiv.
-Require Import morphism action finalg zmodp cyclic center pgroup abelian.
-Require Import matrix mxabelem vector falgebra fieldext separable galois.
-Require ssrnum ssrint algC cyclotomic.
+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 bigop prime finset.
+From mathcomp.fingroup
+Require Import fingroup morphism action.
+From mathcomp.algebra
+Require Import ssralg poly polydiv finalg zmodp cyclic.
+From mathcomp.algebra
+Require Import matrix vector.
+From mathcomp.solvable
+Require Import center pgroup abelian.
+From mathcomp.field
+Require Import falgebra fieldext separable galois.
+Require Import mxabelem.
+
+From mathcomp.algebra Require ssrnum ssrint.
+From mathcomp.field Require algC cyclotomic.
 
 (******************************************************************************)
 (*  Additional constructions and results on finite fields.                    *)
diff --git a/mathcomp/character/inertia.v b/mathcomp/character/inertia.v
index fc33e1a..9a795e8 100644
--- a/mathcomp/character/inertia.v
+++ b/mathcomp/character/inertia.v
@@ -1,10 +1,20 @@
 (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
-Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq path choice div.
-Require Import fintype tuple finfun bigop prime ssralg ssrnum finset fingroup.
-Require Import morphism perm automorphism quotient action zmodp cyclic center.
-Require Import gproduct commutator gseries nilpotent pgroup sylow 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 tuple finfun bigop prime finset.
+From mathcomp.fingroup
+Require Import fingroup morphism perm automorphism quotient action gproduct.
+From mathcomp.algebra
+Require Import ssralg ssrnum zmodp cyclic matrix mxalgebra vector.
+From mathcomp.solvable
+Require Import center commutator gseries nilpotent pgroup sylow maximal.
+From mathcomp.solvable
 Require Import frobenius.
-Require Import matrix mxalgebra mxrepresentation vector algC classfun character.
+From mathcomp.field
+Require Import algC.
+Require Import mxrepresentation classfun character.
 
 Set Implicit Arguments.
 Unset Strict Implicit.
diff --git a/mathcomp/character/integral_char.v b/mathcomp/character/integral_char.v
index d327ac3..14ae4fc 100644
--- a/mathcomp/character/integral_char.v
+++ b/mathcomp/character/integral_char.v
@@ -1,10 +1,19 @@
 (* (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 finset.
-Require Import fingroup morphism perm automorphism quotient action finalg zmodp.
-Require Import commutator cyclic center pgroup sylow gseries nilpotent abelian.
-Require Import ssrnum ssrint polydiv rat matrix mxalgebra intdiv mxpoly.
-Require Import vector falgebra fieldext separable galois algC cyclotomic algnum.
+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 prime finset.
+From mathcomp.fingroup
+Require Import fingroup morphism perm automorphism quotient action gproduct.
+From mathcomp.algebra
+Require Import ssralg poly polydiv finalg zmodp cyclic matrix mxalgebra mxpoly.
+From mathcomp.solvable
+Require Import commutator center pgroup sylow gseries nilpotent abelian.
+From mathcomp.algebra
+Require Import ssrnum ssrint polydiv rat matrix mxalgebra intdiv mxpoly vector.
+From mathcomp.field
+Require Import fieldext separable galois algC cyclotomic algnum falgebra.
 Require Import mxrepresentation classfun character.
 
 (******************************************************************************)
diff --git a/mathcomp/character/mxabelem.v b/mathcomp/character/mxabelem.v
index 188000d..377cb72 100644
--- a/mathcomp/character/mxabelem.v
+++ b/mathcomp/character/mxabelem.v
@@ -1,9 +1,18 @@
 (* (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 finset.
+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 prime finset.
+From mathcomp.fingroup
 Require Import fingroup morphism perm automorphism quotient gproduct action.
-Require Import finalg zmodp commutator cyclic center pgroup gseries nilpotent.
-Require Import sylow maximal abelian matrix mxalgebra mxrepresentation.
+From mathcomp.algebra
+Require Import ssralg poly finalg zmodp cyclic matrix mxalgebra.
+From mathcomp.solvable
+Require Import commutator center pgroup gseries nilpotent.
+From mathcomp.solvable
+Require Import sylow maximal abelian.
+Require Import mxrepresentation.
 
 (******************************************************************************)
 (*   This file completes the theory developed in mxrepresentation.v with the  *)
diff --git a/mathcomp/character/mxrepresentation.v b/mathcomp/character/mxrepresentation.v
index e8bbed3..e947fe0 100644
--- a/mathcomp/character/mxrepresentation.v
+++ b/mathcomp/character/mxrepresentation.v
@@ -1,8 +1,15 @@
 (* (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 polydiv finset.
-Require Import fingroup morphism perm automorphism quotient finalg action zmodp.
-Require Import commutator cyclic center pgroup matrix mxalgebra mxpoly.
+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 prime finset.
+From mathcomp.fingroup
+Require Import fingroup morphism perm automorphism quotient action gproduct.
+From mathcomp.algebra
+Require Import ssralg poly polydiv finalg zmodp cyclic matrix mxalgebra mxpoly.
+From mathcomp.solvable
+Require Import commutator center pgroup.
 
 (******************************************************************************)
 (*  This file provides linkage between classic Group Theory and commutative   *)
diff --git a/mathcomp/character/vcharacter.v b/mathcomp/character/vcharacter.v
index 3ef364d..9071740 100644
--- a/mathcomp/character/vcharacter.v
+++ b/mathcomp/character/vcharacter.v
@@ -1,9 +1,17 @@
 (* (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 finset.
-Require Import fingroup morphism perm automorphism quotient finalg action.
-Require Import gproduct zmodp commutator cyclic center pgroup sylow frobenius.
-Require Import vector ssrnum ssrint intdiv algC algnum.
+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 prime finset.
+From mathcomp.fingroup
+Require Import fingroup morphism perm automorphism quotient action gproduct.
+From mathcomp.algebra
+Require Import ssralg poly finalg zmodp cyclic vector ssrnum ssrint intdiv.
+From mathcomp.solvable
+Require Import sylow pgroup center frobenius.
+From mathcomp.field
+Require Import algnum algC.
 Require Import classfun character integral_char.
 
 Set Implicit Arguments.