diff options
| -rw-r--r-- | mathcomp/algebra/cyclic.v | 10 | ||||
| -rw-r--r-- | mathcomp/algebra/finalg.v | 9 | ||||
| -rw-r--r-- | mathcomp/algebra/fraction.v | 7 | ||||
| -rw-r--r-- | mathcomp/algebra/intdiv.v | 11 | ||||
| -rw-r--r-- | mathcomp/algebra/interval.v | 9 | ||||
| -rw-r--r-- | mathcomp/algebra/matrix.v | 10 | ||||
| -rw-r--r-- | mathcomp/algebra/mxalgebra.v | 10 | ||||
| -rw-r--r-- | mathcomp/algebra/mxpoly.v | 10 | ||||
| -rw-r--r-- | mathcomp/algebra/poly.v | 8 | ||||
| -rw-r--r-- | mathcomp/algebra/polyXY.v | 10 | ||||
| -rw-r--r-- | mathcomp/algebra/polydiv.v | 7 | ||||
| -rw-r--r-- | mathcomp/algebra/rat.v | 7 | ||||
| -rw-r--r-- | mathcomp/algebra/ring_quotient.v | 8 | ||||
| -rw-r--r-- | mathcomp/algebra/ssralg.v | 6 | ||||
| -rw-r--r-- | mathcomp/algebra/ssrint.v | 8 | ||||
| -rw-r--r-- | mathcomp/algebra/ssrnum.v | 9 | ||||
| -rw-r--r-- | mathcomp/algebra/vector.v | 7 | ||||
| -rw-r--r-- | mathcomp/algebra/zmodp.v | 9 |
18 files changed, 112 insertions, 43 deletions
diff --git a/mathcomp/algebra/cyclic.v b/mathcomp/algebra/cyclic.v index ad10492..caeb57f 100644 --- a/mathcomp/algebra/cyclic.v +++ b/mathcomp/algebra/cyclic.v @@ -1,7 +1,11 @@ (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *) -Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq div fintype bigop. -Require Import prime finset fingroup morphism perm automorphism quotient. -Require Import gproduct ssralg finalg zmodp poly. +(*v8.5 From mathcomp.ssreflect *) +Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq. +(*v8.5 From mathcomp.discrete *) +Require Import div fintype bigop prime finset. +(*v8.5 From mathcomp.fingroup *) +Require Import fingroup morphism perm automorphism quotient gproduct. +Require Import ssralg finalg zmodp poly. (******************************************************************************) (* Properties of cyclic groups. *) diff --git a/mathcomp/algebra/finalg.v b/mathcomp/algebra/finalg.v index b903577..d364fc9 100644 --- a/mathcomp/algebra/finalg.v +++ b/mathcomp/algebra/finalg.v @@ -1,6 +1,11 @@ (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *) -Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype. -Require Import ssralg finset fingroup morphism perm action. +(*v8.5 From mathcomp.ssreflect *) +Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq. +(*v8.5 From mathcomp.discrete *) +Require Import choice fintype finset. +(*v8.5 From mathcomp.fingroup *) +Require Import fingroup morphism perm action. +Require Import ssralg. (*****************************************************************************) (* 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 732cc19..446248f 100644 --- a/mathcomp/algebra/fraction.v +++ b/mathcomp/algebra/fraction.v @@ -1,6 +1,9 @@ (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *) -Require Import ssreflect ssrfun ssrbool eqtype ssrnat div seq choice tuple. -Require Import bigop ssralg poly polydiv generic_quotient. +(*v8.5 From mathcomp.ssreflect *) +Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq. +(*v8.5 From mathcomp.discrete *) +Require Import div choice tuple bigop generic_quotient. +Require Import ssralg poly polydiv. (* 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 4f1ce95..bfd4b13 100644 --- a/mathcomp/algebra/intdiv.v +++ b/mathcomp/algebra/intdiv.v @@ -1,7 +1,12 @@ (* (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 ssrnum ssrint rat. -Require Import polydiv finalg perm zmodp matrix mxalgebra vector. +(*v8.5 From mathcomp.ssreflect *) +Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq. +(*v8.5 From mathcomp.discrete *) +Require Import path div choice fintype tuple finfun bigop prime. +(*v8.5 From mathcomp.fingroup *) +Require Import perm. +Require Import ssralg poly ssrnum ssrint rat. +Require Import polydiv finalg zmodp matrix mxalgebra vector. (******************************************************************************) (* This file provides various results on divisibility of integers. *) diff --git a/mathcomp/algebra/interval.v b/mathcomp/algebra/interval.v index 1f59ce2..7bde270 100644 --- a/mathcomp/algebra/interval.v +++ b/mathcomp/algebra/interval.v @@ -1,6 +1,11 @@ (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *) -Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq div choice fintype. -Require Import bigop ssralg finset fingroup zmodp ssrint ssrnum. +(*v8.5 From mathcomp.ssreflect *) +Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq. +(*v8.5 From mathcomp.discrete *) +Require Import div choice fintype bigop finset. +(*v8.5 From mathcomp.fingroup *) +Require Import fingroup. +Require Import ssralg zmodp ssrint 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 ecf5801..e67008d 100644 --- a/mathcomp/algebra/matrix.v +++ b/mathcomp/algebra/matrix.v @@ -1,7 +1,11 @@ (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *) -Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq div choice fintype. -Require Import finfun bigop prime binomial ssralg finset fingroup finalg. -Require Import perm zmodp. +(*v8.5 From mathcomp.ssreflect *) +Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq. +(*v8.5 From mathcomp.discrete *) +Require Import div choice fintype finfun bigop prime binomial finset. +(*v8.5 From mathcomp.fingroup *) +Require Import fingroup perm. +Require Import ssralg finalg zmodp. (******************************************************************************) (* Basic concrete linear algebra : definition of type for matrices, and all *) diff --git a/mathcomp/algebra/mxalgebra.v b/mathcomp/algebra/mxalgebra.v index 54d5588..833a229 100644 --- a/mathcomp/algebra/mxalgebra.v +++ b/mathcomp/algebra/mxalgebra.v @@ -1,7 +1,11 @@ (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *) -Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq div choice fintype. -Require Import finfun bigop prime binomial ssralg finset fingroup finalg. -Require Import perm zmodp matrix. +(*v8.5 From mathcomp.ssreflect *) +Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq. +(*v8.5 From mathcomp.discrete *) +Require Import div choice fintype finfun bigop prime binomial finset. +(*v8.5 From mathcomp.fingroup *) +Require Import fingroup perm. +Require Import 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 7e889a0..8a0b519 100644 --- a/mathcomp/algebra/mxpoly.v +++ b/mathcomp/algebra/mxpoly.v @@ -1,7 +1,11 @@ (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *) -Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq div fintype tuple. -Require Import finfun bigop fingroup perm ssralg zmodp matrix mxalgebra. -Require Import poly polydiv. +(*v8.5 From mathcomp.ssreflect *) +Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq. +(*v8.5 From mathcomp.discrete *) +Require Import div fintype tuple finfun bigop. +(*v8.5 From mathcomp.fingroup *) +Require Import fingroup perm. +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 813f70d..e473f2d 100644 --- a/mathcomp/algebra/poly.v +++ b/mathcomp/algebra/poly.v @@ -1,6 +1,10 @@ (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *) -Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq div choice fintype. -Require Import bigop ssralg binomial. +(*v8.5 From mathcomp.ssreflect *) +Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq. +(*v8.5 From mathcomp.discrete *) +Require Import div choice fintype bigop binomial. +Require Import ssralg. + (******************************************************************************) (* This file provides a library for univariate polynomials over ring *) diff --git a/mathcomp/algebra/polyXY.v b/mathcomp/algebra/polyXY.v index 3d2292e..5abc40d 100644 --- a/mathcomp/algebra/polyXY.v +++ b/mathcomp/algebra/polyXY.v @@ -1,7 +1,11 @@ (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *) -Require Import ssreflect ssrfun ssrbool choice eqtype ssrnat seq div fintype. -Require Import tuple finfun bigop fingroup perm ssralg zmodp matrix mxalgebra. -Require Import poly polydiv mxpoly binomial. +(*v8.5 From mathcomp.ssreflect *) +Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq. +(*v8.5 From mathcomp.discrete *) +Require Import choice div fintype tuple finfun bigop binomial. +(*v8.5 From mathcomp.fingroup *) +Require Import fingroup perm. +Require Import ssralg zmodp matrix mxalgebra poly polydiv mxpoly. (******************************************************************************) (* This file provides additional primitives and theory for bivariate *) diff --git a/mathcomp/algebra/polydiv.v b/mathcomp/algebra/polydiv.v index eca9a27..fa3a132 100644 --- a/mathcomp/algebra/polydiv.v +++ b/mathcomp/algebra/polydiv.v @@ -1,6 +1,9 @@ (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *) -Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype. -Require Import bigop ssralg poly. +(*v8.5 From mathcomp.ssreflect *) +Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq. +(*v8.5 From mathcomp.discrete *) +Require Import bigop choice fintype. +Require Import 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 b2b88d9..342eead 100644 --- a/mathcomp/algebra/rat.v +++ b/mathcomp/algebra/rat.v @@ -1,6 +1,9 @@ (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *) -Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype. -Require Import bigop ssralg div ssrnum ssrint. +(*v8.5 From mathcomp.ssreflect *) +Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq. +(*v8.5 From mathcomp.discrete *) +Require Import div choice fintype bigop. +Require Import ssralg 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 479508c..6f2a2f5 100644 --- a/mathcomp/algebra/ring_quotient.v +++ b/mathcomp/algebra/ring_quotient.v @@ -1,7 +1,9 @@ (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *) -Require Import eqtype choice ssreflect ssrbool ssrnat ssrfun seq. -Require Import ssralg generic_quotient. - +(*v8.5 From mathcomp.ssreflect *) +Require Import ssreflect ssrfun ssrbool ssrnat eqtype seq. +(*v8.5 From mathcomp.discrete *) +Require Import choice generic_quotient. +Require Import ssralg. (******************************************************************************) (* This file describes quotients of algebraic structures. *) diff --git a/mathcomp/algebra/ssralg.v b/mathcomp/algebra/ssralg.v index 5f4592b..3627447 100644 --- a/mathcomp/algebra/ssralg.v +++ b/mathcomp/algebra/ssralg.v @@ -1,6 +1,8 @@ (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *) -Require Import ssreflect ssrfun ssrbool eqtype ssrnat div seq choice fintype. -Require Import finfun bigop prime binomial. +(*v8.5 From mathcomp.ssreflect *) +Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq. +(*v8.5 From mathcomp.discrete *) +Require Import div 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 cbf726e..3281c44 100644 --- a/mathcomp/algebra/ssrint.v +++ b/mathcomp/algebra/ssrint.v @@ -1,6 +1,10 @@ (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *) -Require Import ssreflect ssrfun ssrbool eqtype ssrnat choice seq. -Require Import fintype finfun bigop ssralg ssrnum poly. +(*v8.5 From mathcomp.ssreflect *) +Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq. +(*v8.5 From mathcomp.discrete *) +Require Import choice fintype finfun bigop. +Require Import ssralg ssrnum poly. + Import GRing.Theory Num.Theory. (******************************************************************************) diff --git a/mathcomp/algebra/ssrnum.v b/mathcomp/algebra/ssrnum.v index ab7afd0..19d4c31 100644 --- a/mathcomp/algebra/ssrnum.v +++ b/mathcomp/algebra/ssrnum.v @@ -1,6 +1,11 @@ (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *) -Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq div choice fintype. -Require Import bigop ssralg finset fingroup zmodp poly. +(*v8.5 From mathcomp.ssreflect *) +Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq. +(*v8.5 From mathcomp.discrete *) +Require Import div choice fintype bigop finset. +(*v8.5 From mathcomp.fingroup *) +Require Import fingroup. +Require Import ssralg zmodp poly. (******************************************************************************) (* *) diff --git a/mathcomp/algebra/vector.v b/mathcomp/algebra/vector.v index 2cb59e9..0d4ace0 100644 --- a/mathcomp/algebra/vector.v +++ b/mathcomp/algebra/vector.v @@ -1,6 +1,9 @@ (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *) -Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype bigop. -Require Import finfun tuple ssralg matrix mxalgebra zmodp. +(*v8.5 From mathcomp.ssreflect *) +Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq. +(*v8.5 From mathcomp.discrete *) +Require Import choice fintype bigop finfun tuple. +Require Import ssralg matrix mxalgebra zmodp. (******************************************************************************) (* * Finite dimensional vector spaces *) diff --git a/mathcomp/algebra/zmodp.v b/mathcomp/algebra/zmodp.v index df5b378..614bf10 100644 --- a/mathcomp/algebra/zmodp.v +++ b/mathcomp/algebra/zmodp.v @@ -1,6 +1,11 @@ (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *) -Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq div. -Require Import fintype bigop finset prime fingroup ssralg finalg. +(*v8.5 From mathcomp.ssreflect *) +Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq. +(*v8.5 From mathcomp.discrete *) +Require Import div fintype bigop finset prime. +(*v8.5 From mathcomp.fingroup *) +Require Import fingroup. +Require Import ssralg finalg. (******************************************************************************) (* Definition of the additive group and ring Zp, represented as 'I_p *) |