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/path.v | 1 +
 1 file changed, 1 insertion(+)

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

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