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/fingraph.v | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

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

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