From f24095cfbe19c9ddb5ff3dee17a50f715a98acf5 Mon Sep 17 00:00:00 2001
From: Erik Martin-Dorel
Date: Sun, 25 Feb 2018 23:56:29 +0100
Subject: Add ssrmatching.v transitional file

The content of this file is similar to that of ssrfun.v and aims to
increase compatibility with Coq 8.6+ for third-party libraries that
depend on both math-comp and ssrmatching.v

Close #63
---
 mathcomp/ssreflect/plugin/v8.6/ssreflect.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'mathcomp/ssreflect/plugin')

diff --git a/mathcomp/ssreflect/plugin/v8.6/ssreflect.v b/mathcomp/ssreflect/plugin/v8.6/ssreflect.v
index 079bf72..860f0a1 100644
--- a/mathcomp/ssreflect/plugin/v8.6/ssreflect.v
+++ b/mathcomp/ssreflect/plugin/v8.6/ssreflect.v
@@ -1,7 +1,7 @@
 (* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  *)
 (* Distributed under the terms of CeCILL-B.                                  *)
 Require Import Bool. (* For bool_scope delimiter 'bool'. *)
-Require Import ssrmatching.
+From Coq Require Import ssrmatching.
 Declare ML Module "ssreflect_plugin".
 Set SsrAstVersion.
 
-- 
cgit v1.2.3