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/Makefile.coq-makefile | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'mathcomp/ssreflect/Makefile.coq-makefile')

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