From 7406d43614dda186492f8e8cc184783980aaa969 Mon Sep 17 00:00:00 2001
From: Erik Martin-Dorel
Date: Mon, 13 Nov 2017 23:12:03 +0100
Subject: Update v8.5 plugin to fix math-comp/math-comp#61

---
 mathcomp/ssreflect/Makefile.coq-makefile | 5 +++--
 1 file changed, 3 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 68bfbc2..bf8115e 100644
--- a/mathcomp/ssreflect/Makefile.coq-makefile
+++ b/mathcomp/ssreflect/Makefile.coq-makefile
@@ -4,7 +4,8 @@ define coqmakefile
 	MLLIB=;\
 	EXTRA=;\
 	case $(V) in\
-       	v8.5*|v8.4*)\
+	v8.5*|v8.4*)\
+		$$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 .;\
@@ -13,7 +14,7 @@ define coqmakefile
 		$$LN $(1)/plugin/$(V)/ssrbool.v $(1)/;\
 		$$LN $(1)/plugin/$(V)/ssrfun.v $(1)/;\
 		$$LN $(1)/plugin/$(V)/ssreflect.v $(1)/;\
-		MLLIB=ssreflect_plugin.mllib;\
+		MLLIB="ssrmatching_plugin.mllib ssreflect_plugin.mllib";\
 		EXTRA="ssrmatching.mli ssrmatching.ml4 ssrmatching.v ssreflect.ml4";\
 	;;\
 	v8.6*)\
-- 
cgit v1.2.3