Cleaning Require and Require Imports

18 files changed, 50 insertions, 103 deletions

diff --git a/mathcomp/algebra/countalg.v b/mathcomp/algebra/countalg.v
index 962a296..3aaa02d 100644
--- a/mathcomp/algebra/countalg.v
+++ b/mathcomp/algebra/countalg.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 choice fintype.
-From mathcomp
-Require Import bigop ssralg generic_quotient ring_quotient.
+From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice.
+From mathcomp Require Import fintype bigop ssralg.
+From mathcomp Require Import generic_quotient ring_quotient.
 
 (*****************************************************************************)
 (* This file clones part of ssralg hierachy for countable types; it does not *)
diff --git a/mathcomp/algebra/finalg.v b/mathcomp/algebra/finalg.v
index 9c0025b..f6272f3 100644
--- a/mathcomp/algebra/finalg.v
+++ b/mathcomp/algebra/finalg.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 choice fintype.
-From mathcomp
-Require Import ssralg finset fingroup morphism perm action countalg.
+From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice.
+From mathcomp Require Import fintype finset fingroup morphism perm action.
+From mathcomp Require Import ssralg countalg.
 
 (*****************************************************************************)
 (* This file clones the entire ssralg hierachy for finite types; this allows *)
diff --git a/mathcomp/algebra/fraction.v b/mathcomp/algebra/fraction.v
index dd3ce30..b9aa3ca 100644
--- a/mathcomp/algebra/fraction.v
+++ b/mathcomp/algebra/fraction.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 div seq choice tuple.
-From mathcomp
-Require Import bigop ssralg poly polydiv generic_quotient.
+From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat div seq.
+From mathcomp Require Import choice tuple bigop ssralg poly polydiv.
+From mathcomp Require Import generic_quotient.
 
 (* This file builds the field of fraction of any integral domain. *)
 (* The main result of this file is the existence of the field *)
diff --git a/mathcomp/algebra/intdiv.v b/mathcomp/algebra/intdiv.v
index 1da8313..48e9de8 100644
--- a/mathcomp/algebra/intdiv.v
+++ b/mathcomp/algebra/intdiv.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 ssrbool ssrfun eqtype ssrnat seq path div choice.
-From mathcomp
-Require Import fintype tuple finfun bigop prime ssralg poly ssrnum ssrint rat.
-From mathcomp
-Require Import polydiv finalg perm zmodp matrix mxalgebra vector.
+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 ssrnum ssrint rat matrix.
+From mathcomp Require Import polydiv finalg perm zmodp mxalgebra vector.
 
 (******************************************************************************)
 (* This file provides various results on divisibility of integers.            *)
diff --git a/mathcomp/algebra/interval.v b/mathcomp/algebra/interval.v
index 41767e1..7c1ab8f 100644
--- a/mathcomp/algebra/interval.v
+++ b/mathcomp/algebra/interval.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 ssrfun ssrbool eqtype ssrnat seq div choice fintype.
-From mathcomp
-Require Import bigop ssralg finset fingroup ssrnum.
+From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice.
+From mathcomp Require Import div fintype bigop ssralg finset fingroup ssrnum.
 
 (*****************************************************************************)
 (* This file provide support for intervals in numerical and real domains.    *)
diff --git a/mathcomp/algebra/matrix.v b/mathcomp/algebra/matrix.v
index 2580741..d3142d6 100644
--- a/mathcomp/algebra/matrix.v
+++ b/mathcomp/algebra/matrix.v
@@ -1,12 +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 finfun bigop prime binomial ssralg finset fingroup finalg.
-From mathcomp
-Require Import perm zmodp countalg.
+From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq choice.
+From mathcomp Require Import fintype finfun bigop finset fingroup perm.
+From mathcomp Require Import div prime binomial ssralg finalg zmodp countalg.
 
 (******************************************************************************)
 (* Basic concrete linear algebra : definition of type for matrices, and all   *)
diff --git a/mathcomp/algebra/mxalgebra.v b/mathcomp/algebra/mxalgebra.v
index 7875b83..078fea3 100644
--- a/mathcomp/algebra/mxalgebra.v
+++ b/mathcomp/algebra/mxalgebra.v
@@ -1,12 +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 finfun bigop prime binomial ssralg finset fingroup finalg.
-From mathcomp
-Require Import perm zmodp matrix.
+From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq choice.
+From mathcomp Require Import fintype finfun bigop finset fingroup perm.
+From mathcomp Require Import  div prime binomial ssralg finalg zmodp matrix.
 
 (*****************************************************************************)
 (* In this file we develop the rank and row space theory of matrices, based  *)
diff --git a/mathcomp/algebra/mxpoly.v b/mathcomp/algebra/mxpoly.v
index 710adc6..b95933e 100644
--- a/mathcomp/algebra/mxpoly.v
+++ b/mathcomp/algebra/mxpoly.v
@@ -1,12 +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 fintype tuple.
-From mathcomp
-Require Import finfun bigop fingroup perm ssralg zmodp matrix mxalgebra.
-From mathcomp
-Require Import poly polydiv.
+From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq div.
+From mathcomp Require Import fintype tuple finfun bigop fingroup perm.
+From mathcomp Require Import ssralg zmodp matrix mxalgebra poly polydiv.
 
 (******************************************************************************)
 (*   This file provides basic support for formal computation with matrices,   *)
diff --git a/mathcomp/algebra/poly.v b/mathcomp/algebra/poly.v
index e0feecf..e0a8e5d 100644
--- a/mathcomp/algebra/poly.v
+++ b/mathcomp/algebra/poly.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 div choice fintype.
-From mathcomp
-Require Import bigop ssralg countalg binomial tuple.
+From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq choice.
+From mathcomp Require Import fintype bigop div ssralg countalg binomial tuple.
 
 (******************************************************************************)
 (* This file provides a library for univariate polynomials over ring          *)
diff --git a/mathcomp/algebra/polyXY.v b/mathcomp/algebra/polyXY.v
index 82a4afb..e91b8be 100644
--- a/mathcomp/algebra/polyXY.v
+++ b/mathcomp/algebra/polyXY.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 choice eqtype ssrnat seq div fintype.
-From mathcomp
-Require Import tuple finfun bigop fingroup perm ssralg zmodp matrix mxalgebra.
-From mathcomp
-Require Import poly polydiv mxpoly binomial.
+From mathcomp Require Import ssreflect ssrfun ssrbool eqtype choice ssrnat seq.
+From mathcomp Require Import fintype tuple finfun bigop fingroup perm div.
+From mathcomp Require Import ssralg zmodp matrix mxalgebra.
+From mathcomp Require Import poly polydiv mxpoly binomial.
 
 (******************************************************************************)
 (* This file provides additional primitives and theory for bivariate          *)
diff --git a/mathcomp/algebra/polydiv.v b/mathcomp/algebra/polydiv.v
index 026af3d..6f9d837 100644
--- a/mathcomp/algebra/polydiv.v
+++ b/mathcomp/algebra/polydiv.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 ssrfun ssrbool eqtype ssrnat seq choice fintype.
-From mathcomp
-Require Import bigop ssralg poly.
+From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice.
+From mathcomp Require Import fintype bigop ssralg poly.
 
 (******************************************************************************)
 (* This file provides a library for the basic theory of Euclidean and pseudo- *)
diff --git a/mathcomp/algebra/rat.v b/mathcomp/algebra/rat.v
index 14fde5a..8654fd1 100644
--- a/mathcomp/algebra/rat.v
+++ b/mathcomp/algebra/rat.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 ssrfun ssrbool eqtype ssrnat seq choice fintype.
-From mathcomp
-Require Import bigop ssralg countalg div ssrnum ssrint.
+From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice.
+From mathcomp Require Import fintype bigop ssralg countalg div ssrnum ssrint.
 
 (******************************************************************************)
 (* This file defines a datatype for rational numbers and equips it with a     *)
diff --git a/mathcomp/algebra/ring_quotient.v b/mathcomp/algebra/ring_quotient.v
index 7e708ca..7e6bbf3 100644
--- a/mathcomp/algebra/ring_quotient.v
+++ b/mathcomp/algebra/ring_quotient.v
@@ -1,11 +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 eqtype choice ssreflect ssrbool ssrnat ssrfun seq.
-From mathcomp
-Require Import ssralg generic_quotient.
-
+From mathcomp Require Import ssreflect eqtype choice ssreflect ssrbool ssrnat.
+From mathcomp Require Import ssrfun seq ssralg generic_quotient.
 
 (******************************************************************************)
 (*          This file describes quotients of algebraic structures.            *)
diff --git a/mathcomp/algebra/ssralg.v b/mathcomp/algebra/ssralg.v
index a3b4545..7c74468 100644
--- a/mathcomp/algebra/ssralg.v
+++ b/mathcomp/algebra/ssralg.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 ssrfun ssrbool eqtype ssrnat div seq choice fintype.
-From mathcomp
-Require Import finfun bigop prime binomial.
+From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat div seq.
+From mathcomp Require Import choice fintype finfun bigop prime binomial.
 
 (******************************************************************************)
 (*   The algebraic part of the Algebraic Hierarchy, as described in           *)
diff --git a/mathcomp/algebra/ssrint.v b/mathcomp/algebra/ssrint.v
index b1fa069..1b1eb77 100644
--- a/mathcomp/algebra/ssrint.v
+++ b/mathcomp/algebra/ssrint.v
@@ -1,11 +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 ssrfun ssrbool eqtype ssrnat choice seq.
-From mathcomp
-Require Import fintype finfun bigop ssralg countalg ssrnum poly.
-Import GRing.Theory Num.Theory.
+From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat choice seq.
+From mathcomp Require Import fintype finfun bigop ssralg countalg ssrnum poly.
 
 (******************************************************************************)
 (* This file develops a basic theory of signed integers, defining:            *)
@@ -39,11 +35,11 @@ Import GRing.Theory Num.Theory.
 (* (Posz (x - y)) and (Posz x) - (Posz y) for x, y : nat.                     *)
 (******************************************************************************)
 
-
 Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 
+Import GRing.Theory Num.Theory.
 Delimit Scope int_scope with Z.
 Local Open Scope int_scope.
 
diff --git a/mathcomp/algebra/ssrnum.v b/mathcomp/algebra/ssrnum.v
index fee34a2..6b2a40a 100644
--- a/mathcomp/algebra/ssrnum.v
+++ b/mathcomp/algebra/ssrnum.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 fintype path.
-From mathcomp
-Require Import bigop ssralg finset fingroup poly.
+From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice.
+From mathcomp Require Import div fintype path bigop finset fingroup.
+From mathcomp Require Import ssralg poly.
 
 (******************************************************************************)
 (*                                                                            *)
diff --git a/mathcomp/algebra/vector.v b/mathcomp/algebra/vector.v
index 4766c74..48d7d3e 100644
--- a/mathcomp/algebra/vector.v
+++ b/mathcomp/algebra/vector.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 choice fintype bigop.
-From mathcomp
-Require Import finfun tuple ssralg matrix mxalgebra zmodp.
+From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice.
+From mathcomp Require Import fintype bigop finfun tuple.
+From mathcomp Require Import ssralg matrix mxalgebra zmodp.
 
 (******************************************************************************)
 (*  * Finite dimensional vector spaces                                        *)
diff --git a/mathcomp/algebra/zmodp.v b/mathcomp/algebra/zmodp.v
index 5e931ef..9371721 100644
--- a/mathcomp/algebra/zmodp.v
+++ b/mathcomp/algebra/zmodp.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.
-From mathcomp
-Require Import fintype bigop finset prime fingroup ssralg finalg countalg.
+From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq div.
+From mathcomp Require Import fintype bigop finset prime fingroup.
+From mathcomp Require Import ssralg finalg countalg.
 
 (******************************************************************************)
 (*  Definition of the additive group and ring Zp, represented as 'I_p         *)