Merge pull request #57 from math-comp/archimedean

Address deprecation warnings and clean up the import lists

theories/BGappendixAB.v

@@ -1,18 +1,13 @@
 (* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  *)
 (* Distributed under the terms of CeCILL-B.                                  *)
-Require Import mathcomp.ssreflect.ssreflect.
-From mathcomp
-Require Import ssrbool ssrfun eqtype ssrnat seq div.
-From mathcomp
-Require Import fintype bigop prime finset ssralg fingroup morphism.
-From mathcomp
-Require Import automorphism quotient gfunctor commutator zmodp center pgroup.
-From mathcomp
-Require Import sylow gseries nilpotent abelian maximal.
-From mathcomp
-Require Import matrix mxalgebra mxrepresentation mxabelem.
-From odd_order
-Require Import BGsection1 BGsection2.
+From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq div.
+From mathcomp Require Import fintype bigop prime finset.
+From mathcomp Require Import fingroup morphism automorphism quotient.
+From mathcomp Require Import ssralg zmodp matrix mxalgebra.
+From mathcomp Require Import center gfunctor commutator gseries pgroup.
+From mathcomp Require Import nilpotent sylow abelian maximal.
+From mathcomp Require Import mxrepresentation mxabelem.
+From odd_order Require Import BGsection1 BGsection2.
 
 (******************************************************************************)
 (* This file contains the useful material in B & G, appendices A and B, i.e., *)

theories/BGappendixC.v

@@ -1,20 +1,17 @@
 (* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  *)
 (* Distributed under the terms of CeCILL-B.                                  *)
-Require Import mathcomp.ssreflect.ssreflect.
-From mathcomp
-Require Import ssrbool ssrfun eqtype choice ssrnat seq div fintype tuple finfun.
-From mathcomp
-Require Import bigop order ssralg finset prime binomial poly polydiv.
-From mathcomp
-Require Import fingroup morphism quotient automorphism action finalg zmodp.
-From mathcomp
-Require Import gfunctor gproduct cyclic commutator pgroup abelian frobenius.
-From odd_order
-Require Import BGsection1.
-From mathcomp
-Require Import matrix mxalgebra mxabelem vector falgebra fieldext galois.
-From mathcomp
-Require Import finfield ssrnum algC classfun character integral_char inertia.
+From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq div.
+From mathcomp Require Import choice fintype tuple finfun bigop prime finset.
+From mathcomp Require Import binomial order.
+From mathcomp Require Import fingroup morphism automorphism quotient action.
+From mathcomp Require Import gproduct.
+From mathcomp Require Import ssralg finalg zmodp poly polydiv ssrnum matrix.
+From mathcomp Require Import mxalgebra vector.
+From mathcomp Require Import cyclic gfunctor commutator pgroup abelian.
+From mathcomp Require Import frobenius.
+From mathcomp Require Import falgebra fieldext galois algC finfield.
+From mathcomp Require Import mxabelem classfun character integral_char inertia.
+From odd_order Require Import BGsection1.
 
 Set Implicit Arguments.
 Unset Strict Implicit.

theories/BGsection1.v

@@ -1,18 +1,13 @@
 (* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  *)
 (* Distributed under the terms of CeCILL-B.                                  *)
-Require Import mathcomp.ssreflect.ssreflect.
-From mathcomp
-Require Import ssrbool ssrfun eqtype ssrnat seq path div fintype.
-From mathcomp
-Require Import bigop prime binomial finset fingroup morphism perm automorphism.
-From mathcomp
-Require Import quotient action gproduct gfunctor commutator.
-From mathcomp
-Require Import ssralg finalg zmodp cyclic center pgroup finmodule gseries.
-From mathcomp
-Require Import nilpotent sylow abelian maximal hall extremal.
-From mathcomp
-Require Import matrix mxalgebra mxrepresentation mxabelem.
+From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq path.
+From mathcomp Require Import div fintype bigop prime finset binomial.
+From mathcomp Require Import fingroup morphism perm automorphism quotient.
+From mathcomp Require Import action gproduct ssralg finalg zmodp matrix.
+From mathcomp Require Import mxalgebra.
+From mathcomp Require Import cyclic center gfunctor commutator finmodule.
+From mathcomp Require Import gseries pgroup nilpotent sylow abelian maximal.
+From mathcomp Require Import hall extremal mxrepresentation mxabelem.
 
 (******************************************************************************)
 (* This file contains most of the material in B & G, section 1, including the *)

theories/BGsection10.v

@@ -1,18 +1,13 @@
 (* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  *)
 (* Distributed under the terms of CeCILL-B.                                  *)
-Require Import mathcomp.ssreflect.ssreflect.
-From mathcomp
-Require Import ssrbool ssrfun eqtype ssrnat seq div path fintype.
-From mathcomp
-Require Import bigop finset prime fingroup morphism perm automorphism quotient.
-From mathcomp
-Require Import action gproduct gfunctor pgroup cyclic center commutator.
-From mathcomp
-Require Import gseries nilpotent sylow abelian maximal hall.
-From odd_order
-Require Import BGsection1 BGsection3 BGsection4 BGsection5 BGsection6.
-From odd_order
-Require Import BGsection7 BGsection9.
+From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq path.
+From mathcomp Require Import div fintype bigop prime finset.
+From mathcomp Require Import fingroup morphism perm automorphism quotient.
+From mathcomp Require Import action gproduct.
+From mathcomp Require Import cyclic center gfunctor commutator gseries pgroup.
+From mathcomp Require Import nilpotent sylow abelian maximal hall.
+From odd_order Require Import BGsection1 BGsection3 BGsection4 BGsection5.
+From odd_order Require Import BGsection6 BGsection7 BGsection9.
 
 (******************************************************************************)
 (*   This file covers B & G, section 10, including with the definitions:      *)

theories/BGsection11.v

@@ -1,18 +1,13 @@
 (* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  *)
 (* Distributed under the terms of CeCILL-B.                                  *)
-Require Import mathcomp.ssreflect.ssreflect.
-From mathcomp
-Require Import ssrbool ssrfun eqtype ssrnat seq div path fintype.
-From mathcomp
-Require Import bigop finset prime fingroup morphism perm automorphism quotient.
-From mathcomp
-Require Import action gproduct gfunctor pgroup cyclic center commutator.
-From mathcomp
-Require Import gseries nilpotent sylow abelian maximal hall.
-From odd_order
-Require Import BGsection1 BGsection3 BGsection4 BGsection5 BGsection6.
-From odd_order
-Require Import BGsection7 BGsection10.
+From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq path.
+From mathcomp Require Import div fintype bigop prime finset.
+From mathcomp Require Import fingroup morphism perm automorphism quotient.
+From mathcomp Require Import action gproduct.
+From mathcomp Require Import cyclic center gfunctor commutator gseries pgroup.
+From mathcomp Require Import nilpotent sylow abelian maximal hall.
+From odd_order Require Import BGsection1 BGsection3 BGsection4 BGsection5.
+From odd_order Require Import BGsection6 BGsection7 BGsection10.
 
 (******************************************************************************)
 (*   This file covers B & G, section 11; it has only one definition:          *)

theories/BGsection12.v

@@ -1,18 +1,14 @@
 (* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  *)
 (* Distributed under the terms of CeCILL-B.                                  *)
-Require Import mathcomp.ssreflect.ssreflect.
-From mathcomp
-Require Import ssrbool ssrfun eqtype ssrnat seq choice div fintype.
-From mathcomp
-Require Import path bigop finset prime fingroup morphism perm automorphism.
-From mathcomp
-Require Import quotient action gproduct gfunctor pgroup cyclic commutator.
-From mathcomp
-Require Import center gseries nilpotent sylow abelian maximal hall frobenius.
-From odd_order
-Require Import BGsection1 BGsection3 BGsection4 BGsection5 BGsection6.
-From odd_order
-Require Import BGsection7 BGsection9 BGsection10 BGsection11.
+From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq path.
+From mathcomp Require Import div fintype bigop prime finset.
+From mathcomp Require Import fingroup morphism perm automorphism quotient.
+From mathcomp Require Import action gproduct.
+From mathcomp Require Import cyclic center gfunctor commutator gseries pgroup.
+From mathcomp Require Import nilpotent sylow abelian maximal hall frobenius.
+From odd_order Require Import BGsection1 BGsection3 BGsection4 BGsection5.
+From odd_order Require Import BGsection6 BGsection7 BGsection9 BGsection10.
+From odd_order Require Import BGsection11.
 
 (******************************************************************************)
 (*   This file covers B & G, section 12; it defines the prime sets for the    *)

theories/BGsection13.v

@@ -1,18 +1,14 @@
 (* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  *)
 (* Distributed under the terms of CeCILL-B.                                  *)
-Require Import mathcomp.ssreflect.ssreflect.
-From mathcomp
-Require Import ssrbool ssrfun eqtype ssrnat seq div path fintype.
-From mathcomp
-Require Import bigop finset prime fingroup morphism perm automorphism quotient.
-From mathcomp
-Require Import action gproduct gfunctor pgroup cyclic center commutator.
-From mathcomp
-Require Import gseries nilpotent sylow abelian maximal hall frobenius.
-From odd_order
-Require Import BGsection1 BGsection3 BGsection4 BGsection5 BGsection6.
-From odd_order
-Require Import BGsection7 BGsection9 BGsection10 BGsection12.
+From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq path.
+From mathcomp Require Import div fintype bigop prime finset.
+From mathcomp Require Import fingroup morphism perm automorphism quotient.
+From mathcomp Require Import action gproduct.
+From mathcomp Require Import cyclic center gfunctor commutator gseries pgroup.
+From mathcomp Require Import nilpotent sylow abelian maximal hall frobenius.
+From odd_order Require Import BGsection1 BGsection3 BGsection4 BGsection5.
+From odd_order Require Import BGsection6 BGsection7 BGsection9 BGsection10.
+From odd_order Require Import BGsection12.
 
 (******************************************************************************)
 (*   This file covers B & G, section 13; the title subject of the section,    *)

theories/BGsection14.v

@@ -1,20 +1,14 @@
 (* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  *)
 (* Distributed under the terms of CeCILL-B.                                  *)
-Require Import mathcomp.ssreflect.ssreflect.
-From mathcomp
-Require Import ssrbool ssrfun eqtype ssrnat seq div path fintype bigop order.
-From mathcomp
-Require Import finset prime fingroup morphism perm automorphism quotient.
-From mathcomp
-Require Import action gproduct gfunctor pgroup cyclic center commutator.
-From mathcomp
-Require Import gseries nilpotent sylow abelian maximal hall frobenius.
-From mathcomp
-Require Import ssralg ssrnum ssrint rat.
-From odd_order
-Require Import BGsection1 BGsection3 BGsection4 BGsection5 BGsection6.
-From odd_order
-Require Import BGsection7 BGsection9 BGsection10 BGsection12 BGsection13.
+From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq path.
+From mathcomp Require Import div fintype bigop prime finset order.
+From mathcomp Require Import fingroup morphism perm automorphism quotient.
+From mathcomp Require Import action gproduct ssralg ssrnum ssrint rat.
+From mathcomp Require Import cyclic center gfunctor commutator gseries pgroup.
+From mathcomp Require Import nilpotent sylow abelian maximal hall frobenius.
+From odd_order Require Import BGsection1 BGsection3 BGsection4 BGsection5.
+From odd_order Require Import BGsection6 BGsection7 BGsection9 BGsection10.
+From odd_order Require Import BGsection12 BGsection13.
 
 (******************************************************************************)
 (*   This file covers B & G, section 14, starting with the definition of the  *)

theories/BGsection15.v

@@ -1,20 +1,14 @@
 (* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  *)
 (* Distributed under the terms of CeCILL-B.                                  *)
-Require Import mathcomp.ssreflect.ssreflect.
-From mathcomp
-Require Import ssrbool ssrfun eqtype ssrnat seq choice div fintype.
-From mathcomp
-Require Import path bigop finset prime fingroup morphism perm automorphism.
-From mathcomp
-Require Import quotient action gproduct gfunctor pgroup cyclic commutator.
-From mathcomp
-Require Import center gseries nilpotent sylow abelian maximal hall frobenius.
-From odd_order
-Require Import BGsection1 BGsection2 BGsection3 BGsection4 BGsection5.
-From odd_order
-Require Import BGsection6 BGsection7 BGsection9 BGsection10 BGsection12.
-From odd_order
-Require Import BGsection13 BGsection14.
+From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq path.
+From mathcomp Require Import div choice fintype bigop prime finset.
+From mathcomp Require Import fingroup morphism perm automorphism quotient.
+From mathcomp Require Import action gproduct.
+From mathcomp Require Import cyclic center gfunctor commutator gseries pgroup.
+From mathcomp Require Import nilpotent sylow abelian maximal hall frobenius.
+From odd_order Require Import BGsection1 BGsection2 BGsection3 BGsection4.
+From odd_order Require Import BGsection5 BGsection6 BGsection7 BGsection9.
+From odd_order Require Import BGsection10 BGsection12 BGsection13 BGsection14.
 
 (******************************************************************************)
 (*   This file covers B & G, section 15; it fills in the picture of maximal   *)

theories/BGsection16.v

@@ -1,20 +1,15 @@
 (* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  *)
 (* Distributed under the terms of CeCILL-B.                                  *)
-Require Import mathcomp.ssreflect.ssreflect.
-From mathcomp
-Require Import ssrbool ssrfun eqtype ssrnat seq div path fintype.
-From mathcomp
-Require Import bigop finset prime fingroup morphism perm automorphism quotient.
-From mathcomp
-Require Import action gproduct gfunctor pgroup cyclic center commutator.
-From mathcomp
-Require Import gseries nilpotent sylow abelian maximal hall frobenius.
-From odd_order
-Require Import BGsection1 BGsection2 BGsection3 BGsection4 BGsection5.
-From odd_order
-Require Import BGsection6 BGsection7 BGsection9 BGsection10 BGsection12.
-From odd_order
-Require Import BGsection13 BGsection14 BGsection15.
+From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq path.
+From mathcomp Require Import div fintype bigop prime finset.
+From mathcomp Require Import fingroup morphism perm automorphism quotient.
+From mathcomp Require Import action gproduct.
+From mathcomp Require Import cyclic center gfunctor commutator gseries pgroup.
+From mathcomp Require Import nilpotent sylow abelian maximal hall frobenius.
+From odd_order Require Import BGsection1 BGsection2 BGsection3 BGsection4.
+From odd_order Require Import BGsection5 BGsection6 BGsection7 BGsection9.
+From odd_order Require Import BGsection10 BGsection12 BGsection13 BGsection14.
+From odd_order Require Import BGsection15.
 
 (******************************************************************************)
 (*   This file covers B & G, section 16; it summarises all the results of the *)

theories/BGsection2.v

@@ -1,22 +1,14 @@
 (* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  *)
 (* Distributed under the terms of CeCILL-B.                                  *)
-Require Import mathcomp.ssreflect.ssreflect.
-From mathcomp
-Require Import ssrbool ssrfun eqtype ssrnat seq path div fintype.
-From mathcomp
-Require Import bigop prime binomial finset fingroup morphism perm automorphism.
-From mathcomp
-Require Import quotient action gfunctor commutator gproduct.
-From mathcomp
-Require Import ssralg finalg zmodp cyclic center pgroup gseries nilpotent.
-From mathcomp
-Require Import sylow abelian maximal hall.
-From mathcomp
-Require poly ssrint.
-From mathcomp
-Require Import matrix mxalgebra mxrepresentation mxabelem.
-From odd_order
-Require Import BGsection1.
+From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq path.
+From mathcomp Require Import div fintype bigop prime finset binomial.
+From mathcomp Require Import fingroup morphism perm automorphism quotient.
+From mathcomp Require Import action gproduct ssralg finalg zmodp ssrint poly.
+From mathcomp Require Import matrix mxalgebra.
+From mathcomp Require Import cyclic center gfunctor commutator gseries pgroup.
+From mathcomp Require Import nilpotent sylow abelian maximal.
+From mathcomp Require Import hall mxrepresentation mxabelem.
+From odd_order Require Import BGsection1.
 
 (******************************************************************************)
 (* This file covers the useful material in B & G, Section 2. This excludes    *)

theories/BGsection3.v

@@ -1,20 +1,14 @@
 (* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  *)
 (* Distributed under the terms of CeCILL-B.                                  *)
-Require Import mathcomp.ssreflect.ssreflect.
-From mathcomp
-Require Import ssrbool ssrfun eqtype ssrnat seq path div.
-From mathcomp
-Require Import fintype tuple bigop prime binomial finset ssralg fingroup finalg.
-From mathcomp
-Require Import morphism perm automorphism quotient action commutator gproduct.
-From mathcomp
-Require Import zmodp cyclic gfunctor center pgroup gseries nilpotent sylow.
-From mathcomp
-Require Import finmodule abelian frobenius maximal extremal hall.
-From mathcomp
-Require Import matrix mxalgebra mxrepresentation mxabelem.
-From odd_order
-Require Import wielandt_fixpoint BGsection1 BGsection2.
+From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq path.
+From mathcomp Require Import div fintype tuple bigop prime finset binomial.
+From mathcomp Require Import fingroup morphism perm automorphism quotient.
+From mathcomp Require Import action gproduct.
+From mathcomp Require Import ssralg finalg zmodp matrix mxalgebra.
+From mathcomp Require Import cyclic center gfunctor commutator finmodule.
+From mathcomp Require Import gseries pgroup nilpotent sylow abelian maximal.
+From mathcomp Require Import hall frobenius extremal mxrepresentation mxabelem.
+From odd_order Require Import wielandt_fixpoint BGsection1 BGsection2.
 
 (******************************************************************************)
 (*   This file covers the material in B & G, Section 3.                       *)

theories/BGsection4.v

@@ -1,20 +1,13 @@
 (* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  *)
 (* Distributed under the terms of CeCILL-B.                                  *)
-Require Import mathcomp.ssreflect.ssreflect.
-From mathcomp
-Require Import ssrbool ssrfun eqtype ssrnat seq div.
-From mathcomp
-Require Import fintype finfun bigop ssralg finset prime binomial.
-From mathcomp
-Require Import fingroup morphism automorphism perm quotient action gproduct.
-From mathcomp
-Require Import gfunctor commutator zmodp cyclic center pgroup gseries nilpotent.
-From mathcomp
-Require Import sylow abelian maximal extremal hall.
-From mathcomp
-Require Import matrix mxalgebra mxrepresentation mxabelem.
-From odd_order
-Require Import BGsection1 BGsection2.
+From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq div.
+From mathcomp Require Import fintype finfun bigop prime finset binomial.
+From mathcomp Require Import fingroup morphism perm automorphism quotient.
+From mathcomp Require Import action gproduct ssralg zmodp matrix mxalgebra.
+From mathcomp Require Import cyclic center gfunctor commutator.
+From mathcomp Require Import gseries pgroup nilpotent sylow abelian maximal.
+From mathcomp Require Import hall extremal mxrepresentation mxabelem.
+From odd_order Require Import BGsection1 BGsection2.
 
 (******************************************************************************)
 (*   This file covers B & G, Section 4, i.e., the proof of structure theorems *)