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/Make                              | 1 +
 mathcomp/ssreflect/Make                    | 1 +
 mathcomp/ssreflect/Makefile.coq-makefile   | 4 ++--
 mathcomp/ssreflect/plugin/v8.6/ssreflect.v | 2 +-
 mathcomp/ssreflect/ssrmatching.v           | 1 +
 5 files changed, 6 insertions(+), 3 deletions(-)
 create mode 100644 mathcomp/ssreflect/ssrmatching.v

(limited to 'mathcomp')

diff --git a/mathcomp/Make b/mathcomp/Make
index d3c7642..1db29ba 100644
--- a/mathcomp/Make
+++ b/mathcomp/Make
@@ -130,6 +130,7 @@ ssreflect/ssreflect.v
 ssreflect/ssrfun.v
 ssreflect/ssrnat.v
 ssreflect/ssrnotations.v
+ssreflect/ssrmatching.v
 ssreflect/tuple.v
 ssrtest/absevarprop.v
 ssrtest/abstract_var2.v
diff --git a/mathcomp/ssreflect/Make b/mathcomp/ssreflect/Make
index fc596ab..c529f21 100644
--- a/mathcomp/ssreflect/Make
+++ b/mathcomp/ssreflect/Make
@@ -18,6 +18,7 @@ path.v
 prime.v
 tuple.v
 ssrnotations.v
+ssrmatching.v
 
 -I .
 -R . mathcomp.ssreflect
diff --git a/mathcomp/ssreflect/Makefile.coq-makefile b/mathcomp/ssreflect/Makefile.coq-makefile
index bf8115e..ba0e5d7 100644
--- a/mathcomp/ssreflect/Makefile.coq-makefile
+++ b/mathcomp/ssreflect/Makefile.coq-makefile
@@ -8,14 +8,14 @@ define coqmakefile
 		$$LN $(1)/plugin/$(V)/ssrmatching_plugin.mllib .;\
 		$$LN $(1)/plugin/$(V)/ssrmatching.mli .;\
 		$$LN $(1)/plugin/$(V)/ssrmatching.ml4 .;\
-		$$LN $(1)/plugin/$(V)/ssrmatching.v .;\
+		$$LN $(1)/plugin/$(V)/ssrmatching.v $(1)/;\
 		$$LN $(1)/plugin/$(V)/ssreflect_plugin.mllib .;\
 		$$LN $(1)/plugin/$(V)/ssreflect.ml4 .;\
 		$$LN $(1)/plugin/$(V)/ssrbool.v $(1)/;\
 		$$LN $(1)/plugin/$(V)/ssrfun.v $(1)/;\
 		$$LN $(1)/plugin/$(V)/ssreflect.v $(1)/;\
 		MLLIB="ssrmatching_plugin.mllib ssreflect_plugin.mllib";\
-		EXTRA="ssrmatching.mli ssrmatching.ml4 ssrmatching.v ssreflect.ml4";\
+		EXTRA="ssrmatching.mli ssrmatching.ml4 ssreflect.ml4";\
 	;;\
 	v8.6*)\
 		$$LN $(1)/plugin/$(V)/ssreflect_plugin.mlpack .;\
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.
 
diff --git a/mathcomp/ssreflect/ssrmatching.v b/mathcomp/ssreflect/ssrmatching.v
new file mode 100644
index 0000000..9493dfb
--- /dev/null
+++ b/mathcomp/ssreflect/ssrmatching.v
@@ -0,0 +1 @@
+From Coq Require Export ssrmatching.
-- 
cgit v1.2.3