packaging for v8.5

math-comp · Apr 8, 2015 · 858957a · 858957a
1 parent 737f79e
commit 858957a
Show file tree

Hide file tree

Showing 8 changed files with 37 additions and 14 deletions.
diff --git a/mathcomp/fingroup/action.v b/mathcomp/fingroup/action.v
@@ -1,6 +1,9 @@
 (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
-Require Import ssreflect ssrbool ssrfun eqtype ssrnat div seq fintype.
-Require Import bigop finset fingroup morphism perm automorphism quotient.
+(*v8.5 From mathcomp.ssreflect *)
+Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq.
+(*v8.5 From mathcomp.discrete *)
+Require Import div fintype bigop finset.
+Require Import fingroup morphism perm automorphism quotient.
 
 (******************************************************************************)
 (* Group action: orbits, stabilisers, transitivity.                           *)

diff --git a/mathcomp/fingroup/automorphism.v b/mathcomp/fingroup/automorphism.v
@@ -1,5 +1,8 @@
 (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
-Require Import ssreflect ssrbool ssrfun eqtype ssrnat fintype finset.
+(*v8.5 From mathcomp.ssreflect *)
+Require Import ssreflect ssrbool ssrfun eqtype ssrnat.
+(*v8.5 From mathcomp.discrete *)
+Require Import fintype finset.
 Require Import fingroup perm morphism.
 
 (******************************************************************************)

diff --git a/mathcomp/fingroup/fingroup.v b/mathcomp/fingroup/fingroup.v
@@ -1,6 +1,8 @@
 (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
-Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq choice fintype.
-Require Import div path bigop prime finset.
+(*v8.5 From mathcomp.ssreflect *)
+Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq.
+(*v8.5 From mathcomp.discrete *)
+Require Import  choice 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
@@ -1,6 +1,9 @@
 (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
-Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq div choice fintype.
-Require Import bigop finset fingroup morphism quotient action.
+(*v8.5 From mathcomp.ssreflect *)
+Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq.
+(*v8.5 From mathcomp.discrete *)
+Require Import div choice fintype bigop finset.
+Require Import fingroup morphism quotient action.
 
 (******************************************************************************)
 (*  Partial, semidirect, central, and direct products.                        *)

diff --git a/mathcomp/fingroup/morphism.v b/mathcomp/fingroup/morphism.v
@@ -1,6 +1,9 @@
 (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
-Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq choice fintype finfun.
-Require Import bigop finset fingroup.
+(*v8.5 From mathcomp.ssreflect *)
+Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq.
+(*v8.5 From mathcomp.discrete *)
+Require Import choice fintype finfun bigop finset.
+Require Import fingroup.
 
 (******************************************************************************)
 (* This file contains the definitions of:                                     *)

diff --git a/mathcomp/fingroup/perm.v b/mathcomp/fingroup/perm.v
@@ -1,6 +1,9 @@
 (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
-Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq path choice fintype.
-Require Import tuple finfun bigop finset binomial fingroup.
+(*v8.5 From mathcomp.ssreflect *)
+Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq.
+(*v8.5 From mathcomp.discrete *)
+Require Import path choice fintype tuple finfun bigop finset binomial.
+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
@@ -1,5 +1,8 @@
 (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
-Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype finset.
+(*v8.5 From mathcomp.ssreflect *)
+Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq.
+(*v8.5 From mathcomp.discrete *)
+Require Import fintype finset.
 Require Import fingroup morphism.
 
 (******************************************************************************)

diff --git a/mathcomp/fingroup/quotient.v b/mathcomp/fingroup/quotient.v
@@ -1,6 +1,9 @@
 (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
-Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq div choice.
-Require Import fintype prime finset fingroup morphism automorphism.
+(*v8.5 From mathcomp.ssreflect *)
+Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq.
+(*v8.5 From mathcomp.discrete *)
+Require Import div choice fintype prime finset.
+Require Import fingroup morphism automorphism.
 
 (******************************************************************************)
 (* This file contains the definitions of:                                     *)