packaging for v8.5

8 files changed, 37 insertions, 14 deletions

diff --git a/mathcomp/fingroup/action.v b/mathcomp/fingroup/action.v
index 902e9ca..09c7d75 100644
--- 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
index 1644ebf..d61928b 100644
--- 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
index fe78559..40b5137 100644
--- 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
index 924779f..3c69df5 100644
--- 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
index 7013264..e7ce6b1 100644
--- 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
index 9c31176..ec6df27 100644
--- 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
index 46658d5..a7a0efe 100644
--- 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
index 6688509..204d75e 100644
--- 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:                                     *)