Merge pull request #336 from CohenCyril/clean_require

Cleaning Require and Require Imports

10 files changed, 49 insertions, 86 deletions

diff --git a/mathcomp/field/algC.v b/mathcomp/field/algC.v
index ae60027..86e9e30 100644
--- a/mathcomp/field/algC.v
+++ b/mathcomp/field/algC.v
@@ -1,14 +1,10 @@
 (* (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 ssrnat eqtype seq choice div fintype.
-From mathcomp
-Require Import path bigop finset prime ssralg poly polydiv mxpoly.
-From mathcomp
-Require Import generic_quotient countalg closed_field ssrnum ssrint rat intdiv.
-From mathcomp
-Require Import algebraics_fundamentals.
+From mathcomp Require Import ssreflect ssrbool ssrfun ssrnat eqtype seq choice.
+From mathcomp Require Import div fintype path bigop finset prime ssralg poly.
+From mathcomp Require Import polydiv mxpoly generic_quotient countalg ssrnum.
+From mathcomp Require Import closed_field ssrint rat intdiv.
+From mathcomp Require Import algebraics_fundamentals.
 
 (******************************************************************************)
 (* This file provides an axiomatic construction of the algebraic numbers.     *)
diff --git a/mathcomp/field/algebraics_fundamentals.v b/mathcomp/field/algebraics_fundamentals.v
index ad2388a..6a28884 100644
--- a/mathcomp/field/algebraics_fundamentals.v
+++ b/mathcomp/field/algebraics_fundamentals.v
@@ -1,16 +1,11 @@
 (* (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 ssrnat eqtype seq choice div fintype.
-From mathcomp
-Require Import path tuple bigop finset prime ssralg poly polydiv mxpoly.
-From mathcomp
-Require Import countalg closed_field ssrnum ssrint rat intdiv.
-From mathcomp
-Require Import fingroup finalg zmodp cyclic pgroup sylow.
-From mathcomp
-Require Import vector falgebra fieldext separable galois.
+From mathcomp Require Import ssreflect ssrbool ssrfun ssrnat eqtype seq choice.
+From mathcomp Require Import div fintype path tuple bigop finset prime ssralg.
+From mathcomp Require Import poly polydiv mxpoly countalg closed_field ssrnum.
+From mathcomp Require Import ssrint rat intdiv fingroup finalg zmodp cyclic.
+From mathcomp Require Import pgroup sylow vector falgebra fieldext separable.
+From mathcomp Require Import galois.
 
 (******************************************************************************)
 (*   The main result in this file is the existence theorem that underpins the *)
diff --git a/mathcomp/field/algnum.v b/mathcomp/field/algnum.v
index 3053eb9..144a82e 100644
--- a/mathcomp/field/algnum.v
+++ b/mathcomp/field/algnum.v
@@ -1,14 +1,11 @@
 (* (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 choice.
-From mathcomp
-Require Import fintype tuple finfun bigop prime ssralg finalg zmodp poly.
-From mathcomp
-Require Import ssrnum ssrint rat polydiv intdiv algC matrix mxalgebra mxpoly.
-From mathcomp
-Require Import vector falgebra fieldext separable galois cyclotomic.
+From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq path.
+From mathcomp Require Import div choice fintype tuple finfun bigop prime.
+From mathcomp Require Import ssralg finalg zmodp poly ssrnum ssrint rat.
+From mathcomp Require Import polydiv intdiv algC matrix mxalgebra mxpoly.
+From mathcomp Require Import vector falgebra fieldext separable galois.
+From mathcomp Require Import cyclotomic.
 
 (******************************************************************************)
 (* This file provides a few basic results and constructions in algebraic      *)
diff --git a/mathcomp/field/closed_field.v b/mathcomp/field/closed_field.v
index c338002..b55a48e 100644
--- a/mathcomp/field/closed_field.v
+++ b/mathcomp/field/closed_field.v
@@ -1,10 +1,8 @@
 (* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  *)
 (* Distributed under the terms of CeCILL-B.                                  *)
-Require Import mathcomp.ssreflect.ssreflect.
-From mathcomp
-Require Import ssrfun ssrbool eqtype choice ssrnat seq fintype generic_quotient.
-From mathcomp
-Require Import bigop ssralg poly polydiv matrix mxpoly countalg ring_quotient.
+From mathcomp Require Import ssreflect ssrfun ssrbool eqtype choice ssrnat seq.
+From mathcomp Require Import fintype generic_quotient bigop ssralg poly.
+From mathcomp Require Import polydiv matrix mxpoly countalg ring_quotient.
 
 (******************************************************************************)
 (* This files contains two main contributions:                                *)
diff --git a/mathcomp/field/cyclotomic.v b/mathcomp/field/cyclotomic.v
index afb0b0b..dcb4a5b 100644
--- a/mathcomp/field/cyclotomic.v
+++ b/mathcomp/field/cyclotomic.v
@@ -1,16 +1,10 @@
 (* (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 choice.
-From mathcomp
-Require Import fintype tuple finfun bigop prime ssralg poly finset.
-From mathcomp
-Require Import fingroup finalg zmodp cyclic.
-From mathcomp
-Require Import ssrnum ssrint polydiv rat intdiv.
-From mathcomp
-Require Import mxpoly vector falgebra fieldext separable galois algC.
+From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq path.
+From mathcomp Require Import div choice fintype tuple finfun bigop prime.
+From mathcomp Require Import ssralg poly finset fingroup finalg zmodp cyclic.
+From mathcomp Require Import ssrnum ssrint polydiv rat intdiv mxpoly.
+From mathcomp Require Import vector falgebra fieldext separable galois algC.
 
 (******************************************************************************)
 (* This file provides few basic properties of cyclotomic polynomials.         *)
diff --git a/mathcomp/field/falgebra.v b/mathcomp/field/falgebra.v
index 53a27f0..2a8dddc 100644
--- a/mathcomp/field/falgebra.v
+++ b/mathcomp/field/falgebra.v
@@ -1,10 +1,8 @@
 (* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  *)
 (* Distributed under the terms of CeCILL-B.                                  *)
-Require Import mathcomp.ssreflect.ssreflect.
-From mathcomp
-Require Import ssrfun ssrbool eqtype ssrnat seq path choice fintype.
-From mathcomp
-Require Import div tuple finfun bigop ssralg finalg zmodp matrix vector poly.
+From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq path.
+From mathcomp Require Import choice fintype div tuple finfun bigop ssralg.
+From mathcomp Require Import finalg zmodp matrix vector poly.
 
 (******************************************************************************)
 (* Finite dimensional free algebras, usually known as F-algebras.             *)
diff --git a/mathcomp/field/fieldext.v b/mathcomp/field/fieldext.v
index 7c89607..bb566bb 100644
--- a/mathcomp/field/fieldext.v
+++ b/mathcomp/field/fieldext.v
@@ -1,12 +1,9 @@
 (* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  *)
 (* Distributed under the terms of CeCILL-B.                                  *)
-Require Import mathcomp.ssreflect.ssreflect.
-From mathcomp
-Require Import ssrfun ssrbool eqtype ssrnat seq div choice fintype.
-From mathcomp
-Require Import tuple finfun bigop ssralg finalg zmodp matrix vector falgebra.
-From mathcomp
-Require Import poly polydiv mxpoly generic_quotient.
+From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq div.
+From mathcomp Require Import choice fintype tuple finfun bigop ssralg finalg.
+From mathcomp Require Import zmodp matrix vector falgebra poly polydiv mxpoly.
+From mathcomp Require Import generic_quotient.
 
 (******************************************************************************)
 (*  * Finite dimensional field extentions                                     *)
diff --git a/mathcomp/field/finfield.v b/mathcomp/field/finfield.v
index 4197a2e..00a7bad 100644
--- a/mathcomp/field/finfield.v
+++ b/mathcomp/field/finfield.v
@@ -1,16 +1,11 @@
 (* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  *)
 (* Distributed under the terms of CeCILL-B.                                  *)
-Require Import mathcomp.ssreflect.ssreflect.
-From mathcomp
-Require Import ssrfun ssrbool eqtype ssrnat seq choice fintype div.
-From mathcomp
-Require Import tuple bigop prime finset fingroup ssralg poly polydiv.
-From mathcomp
-Require Import morphism action finalg zmodp cyclic center pgroup abelian.
-From mathcomp
-Require Import matrix mxpoly vector falgebra fieldext separable galois.
-From mathcomp
-Require ssrnum ssrint algC cyclotomic.
+From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice.
+From mathcomp Require Import fintype div tuple bigop prime finset fingroup.
+From mathcomp Require Import ssralg poly polydiv morphism action finalg zmodp.
+From mathcomp Require Import cyclic center pgroup abelian matrix mxpoly vector.
+From mathcomp Require Import falgebra fieldext separable galois.
+From mathcomp Require ssrnum ssrint algC cyclotomic.
 
 (******************************************************************************)
 (*  Additional constructions and results on finite fields.                    *)
diff --git a/mathcomp/field/galois.v b/mathcomp/field/galois.v
index fb96ffe..459250f 100644
--- a/mathcomp/field/galois.v
+++ b/mathcomp/field/galois.v
@@ -1,14 +1,10 @@
 (* (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 choice fintype.
-From mathcomp
-Require Import tuple finfun bigop ssralg poly polydiv.
-From mathcomp
-Require Import finset fingroup morphism quotient perm action zmodp cyclic.
-From mathcomp
-Require Import matrix mxalgebra vector falgebra fieldext separable.
+From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq div.
+From mathcomp Require Import choice fintype tuple finfun bigop ssralg poly.
+From mathcomp Require Import polydiv finset fingroup morphism quotient perm.
+From mathcomp Require Import action zmodp cyclic matrix mxalgebra vector.
+From mathcomp Require Import falgebra fieldext separable.
 
 (******************************************************************************)
 (* This file develops some basic Galois field theory, defining:               *)
diff --git a/mathcomp/field/separable.v b/mathcomp/field/separable.v
index 528b314..a482632 100644
--- a/mathcomp/field/separable.v
+++ b/mathcomp/field/separable.v
@@ -1,14 +1,11 @@
 (* (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 choice fintype.
-From mathcomp
-Require Import tuple finfun bigop finset prime binomial ssralg poly polydiv.
-From mathcomp
-Require Import fingroup perm morphism quotient gproduct finalg zmodp cyclic.
-From mathcomp
-Require Import matrix mxalgebra mxpoly polyXY vector falgebra fieldext.
+From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq div.
+From mathcomp Require Import choice fintype tuple finfun bigop finset prime.
+From mathcomp Require Import binomial ssralg poly polydiv fingroup perm.
+From mathcomp Require Import morphism quotient gproduct finalg zmodp cyclic.
+From mathcomp Require Import matrix mxalgebra mxpoly polyXY vector falgebra.
+From mathcomp Require Import fieldext.
 
 (******************************************************************************)
 (* This file provides a theory of separable and inseparable field extensions. *)