From 9fa572c64085bc020edee574a694fe0805fefdfa Mon Sep 17 00:00:00 2001
From: Cyril Cohen
Date: Fri, 3 Apr 2015 17:22:31 +0200
Subject: prepared discrete for compilation in v8.5

---
 mathcomp/discrete/binomial.v | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'mathcomp/discrete/binomial.v')

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:                                     *)
-- 
cgit v1.2.3