prepared discrete for compilation in v8.5

13 files changed, 30 insertions, 15 deletions

diff --git a/mathcomp/discrete/all.v b/mathcomp/discrete/all.v
index 8412bdb..dfa8536 100644
--- a/mathcomp/discrete/all.v
+++ b/mathcomp/discrete/all.v
@@ -1,4 +1,3 @@
-Require Export mathcomp.ssreflect.all.
 Require Export choice.
 Require Export path.
 Require Export div.
diff --git a/mathcomp/discrete/bigop.v b/mathcomp/discrete/bigop.v
index 88bf4d2..b6d77ec 100644
--- a/mathcomp/discrete/bigop.v
+++ b/mathcomp/discrete/bigop.v
@@ -1,6 +1,7 @@
 (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
-Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq path div fintype.
-Require Import tuple finfun.
+(*v8.5 From mathcomp.ssreflect  *)
+Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq.
+Require Import  path div fintype tuple finfun.
 
 (******************************************************************************)
 (* This file provides a generic definition for iterating an operator over a   *)
diff --git a/mathcomp/discrete/binomial.v b/mathcomp/discrete/binomial.v
index 756a8f9..5656b30 100644
--- a/mathcomp/discrete/binomial.v
+++ b/mathcomp/discrete/binomial.v
@@ -1,6 +1,7 @@
 (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
-Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq path div.
-Require Import fintype tuple finfun bigop prime finset.
+(*v8.5 From mathcomp.ssreflect  *)
+Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq.
+Require Import  path div fintype tuple finfun bigop prime finset.
 
 (******************************************************************************)
 (* This files contains the definition of:                                     *)
diff --git a/mathcomp/discrete/choice.v b/mathcomp/discrete/choice.v
index 96b549c..cfd0b58 100644
--- a/mathcomp/discrete/choice.v
+++ b/mathcomp/discrete/choice.v
@@ -1,4 +1,5 @@
 (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
+(*v8.5 From mathcomp.ssreflect   *)
 Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq.
 
 (******************************************************************************)
diff --git a/mathcomp/discrete/div.v b/mathcomp/discrete/div.v
index d06a8e3..0d94936 100644
--- a/mathcomp/discrete/div.v
+++ b/mathcomp/discrete/div.v
@@ -1,4 +1,5 @@
 (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
+(*v8.5 From mathcomp.ssreflect  *)
 Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq.
 
 (******************************************************************************)
diff --git a/mathcomp/discrete/finfun.v b/mathcomp/discrete/finfun.v
index f880260..e6c6afc 100644
--- a/mathcomp/discrete/finfun.v
+++ b/mathcomp/discrete/finfun.v
@@ -1,5 +1,7 @@
 (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
-Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype tuple.
+(*v8.5 From mathcomp.ssreflect  *)
+Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq.
+Require Import choice fintype tuple.
 
 (******************************************************************************)
 (* This file implements a type for functions with a finite domain:            *)
diff --git a/mathcomp/discrete/fingraph.v b/mathcomp/discrete/fingraph.v
index 403d1ca..d445510 100644
--- a/mathcomp/discrete/fingraph.v
+++ b/mathcomp/discrete/fingraph.v
@@ -1,5 +1,7 @@
 (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
-Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq path fintype.
+(*v8.5 From mathcomp.ssreflect  *)
+Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq.
+Require Import path fintype.
 
 (******************************************************************************)
 (* This file develops the theory of finite graphs represented by an "edge"    *)
diff --git a/mathcomp/discrete/finset.v b/mathcomp/discrete/finset.v
index 54dacc0..5067701 100644
--- a/mathcomp/discrete/finset.v
+++ b/mathcomp/discrete/finset.v
@@ -1,6 +1,7 @@
 (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
-Require Import ssreflect ssrbool ssrfun eqtype ssrnat div seq choice fintype.
-Require Import finfun bigop.
+(*v8.5 From mathcomp.ssreflect  *)
+Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq.
+Require Import bigop choice fintype div finfun.
 
 (******************************************************************************)
 (* This file defines a type for sets over a finite Type, similar to the type  *)
diff --git a/mathcomp/discrete/fintype.v b/mathcomp/discrete/fintype.v
index 63d5e84..5783e43 100644
--- a/mathcomp/discrete/fintype.v
+++ b/mathcomp/discrete/fintype.v
@@ -1,5 +1,7 @@
 (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
-Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice.
+(*v8.5 From mathcomp.ssreflect  *)
+Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq.
+Require Import choice.
 
 (******************************************************************************)
 (*    The Finite interface describes Types with finitely many elements,       *)
diff --git a/mathcomp/discrete/generic_quotient.v b/mathcomp/discrete/generic_quotient.v
index 1d9bd56..c22fa67 100644
--- a/mathcomp/discrete/generic_quotient.v
+++ b/mathcomp/discrete/generic_quotient.v
@@ -1,7 +1,8 @@
 (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
 (* -*- coding : utf-8 -*- *)
-
-Require Import ssreflect ssrfun ssrbool eqtype ssrnat choice seq fintype.
+(*v8.5 From mathcomp.ssreflect  *)
+Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq.
+Require Import choice fintype.
 
 (*****************************************************************************)
 (* Provided a base type T, this files defines an interface for quotients Q   *)
diff --git a/mathcomp/discrete/path.v b/mathcomp/discrete/path.v
index 804e673..85746a4 100644
--- a/mathcomp/discrete/path.v
+++ b/mathcomp/discrete/path.v
@@ -1,4 +1,5 @@
 (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
+(*v8.5 From mathcomp.ssreflect  *)
 Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq.
 
 (******************************************************************************)
diff --git a/mathcomp/discrete/prime.v b/mathcomp/discrete/prime.v
index fa39012..77edad1 100644
--- a/mathcomp/discrete/prime.v
+++ b/mathcomp/discrete/prime.v
@@ -1,6 +1,7 @@
 (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
-Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq path fintype.
-Require Import div bigop.
+(*v8.5 From mathcomp.ssreflect  *)
+Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq.
+Require Import path fintype div bigop.
 
 (******************************************************************************)
 (* This file contains the definitions of:                                     *)
diff --git a/mathcomp/discrete/tuple.v b/mathcomp/discrete/tuple.v
index ba64bd0..f746dd1 100644
--- a/mathcomp/discrete/tuple.v
+++ b/mathcomp/discrete/tuple.v
@@ -1,5 +1,7 @@
 (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
-Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype.
+(*v8.5 From mathcomp.ssreflect  *)
+Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq.
+Require Import choice fintype.
 
 Set Implicit Arguments.
 Unset Strict Implicit.