prepared discrete for compilation in v8.5

math-comp · Apr 3, 2015 · 9fa572c · 9fa572c
1 parent 9859058
commit 9fa572c
Show file tree

Hide file tree

Showing 13 changed files with 30 additions and 15 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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.