Merge pull request #336 from CohenCyril/clean_require

Cleaning Require and Require Imports

8 files changed, 20 insertions, 40 deletions

diff --git a/mathcomp/fingroup/action.v b/mathcomp/fingroup/action.v
index e1f64c8..a365c28 100644
--- a/mathcomp/fingroup/action.v
+++ b/mathcomp/fingroup/action.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 ssrbool ssrfun eqtype ssrnat div seq fintype.
-From mathcomp
-Require Import bigop finset fingroup morphism perm automorphism quotient.
+From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat div seq.
+From mathcomp Require Import fintype bigop finset fingroup morphism perm.
+From mathcomp Require Import automorphism quotient.
 
 (******************************************************************************)
 (* Group action: orbits, stabilisers, transitivity.                           *)
diff --git a/mathcomp/fingroup/automorphism.v b/mathcomp/fingroup/automorphism.v
index 5f28b7d..009e723 100644
--- a/mathcomp/fingroup/automorphism.v
+++ b/mathcomp/fingroup/automorphism.v
@@ -1,10 +1,7 @@
 (* (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 fintype finset.
-From mathcomp
-Require Import fingroup perm morphism.
+From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat fintype.
+From mathcomp Require Import finset fingroup perm morphism.
 
 (******************************************************************************)
 (* Group automorphisms and characteristic subgroups.                          *)
diff --git a/mathcomp/fingroup/fingroup.v b/mathcomp/fingroup/fingroup.v
index 95b66b7..65af825 100644
--- a/mathcomp/fingroup/fingroup.v
+++ b/mathcomp/fingroup/fingroup.v
@@ -1,10 +1,7 @@
 (* (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 fintype.
-From mathcomp
-Require Import div path bigop prime finset.
+From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq choice.
+From mathcomp Require Import fintype div path bigop prime finset.
 
 (******************************************************************************)
 (* This file defines the main interface for finite groups :                   *)
diff --git a/mathcomp/fingroup/gproduct.v b/mathcomp/fingroup/gproduct.v
index 22c19d4..676daf0 100644
--- a/mathcomp/fingroup/gproduct.v
+++ b/mathcomp/fingroup/gproduct.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 ssrbool ssrfun eqtype ssrnat seq div choice fintype.
-From mathcomp
-Require Import bigop finset fingroup morphism quotient action.
+From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq div.
+From mathcomp Require Import choice fintype bigop finset fingroup morphism.
+From mathcomp Require Import quotient action.
 
 (******************************************************************************)
 (*  Partial, semidirect, central, and direct products.                        *)
diff --git a/mathcomp/fingroup/morphism.v b/mathcomp/fingroup/morphism.v
index aa2a809..ef707e1 100644
--- a/mathcomp/fingroup/morphism.v
+++ b/mathcomp/fingroup/morphism.v
@@ -1,10 +1,7 @@
 (* (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 fintype finfun.
-From mathcomp
-Require Import bigop finset fingroup.
+From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq choice.
+From mathcomp Require Import fintype finfun bigop finset fingroup.
 
 (******************************************************************************)
 (* This file contains the definitions of:                                     *)
diff --git a/mathcomp/fingroup/perm.v b/mathcomp/fingroup/perm.v
index 8c97ab1..33bf82c 100644
--- a/mathcomp/fingroup/perm.v
+++ b/mathcomp/fingroup/perm.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 tuple finfun bigop finset binomial fingroup.
+From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq path.
+From mathcomp Require Import choice fintype tuple finfun bigop finset binomial.
+From mathcomp Require Import fingroup.
 
 (******************************************************************************)
 (* This file contains the definition and properties associated to the group   *)
diff --git a/mathcomp/fingroup/presentation.v b/mathcomp/fingroup/presentation.v
index 7e3ad3c..af453aa 100644
--- a/mathcomp/fingroup/presentation.v
+++ b/mathcomp/fingroup/presentation.v
@@ -1,10 +1,7 @@
 (* (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 fintype finset.
-From mathcomp
-Require Import fingroup morphism.
+From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq.
+From mathcomp Require Import fintype finset fingroup morphism.
 
 (******************************************************************************)
 (* Support for generator-and-relation presentations of groups. We provide the *)
diff --git a/mathcomp/fingroup/quotient.v b/mathcomp/fingroup/quotient.v
index 61b0cd9..f73fda5 100644
--- a/mathcomp/fingroup/quotient.v
+++ b/mathcomp/fingroup/quotient.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 div choice.
-From mathcomp
-Require Import fintype prime finset fingroup morphism automorphism.
+From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq div.
+From mathcomp Require Import choice fintype prime finset fingroup morphism.
+From mathcomp Require Import automorphism.
 
 (******************************************************************************)
 (* This file contains the definitions of:                                     *)