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

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

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