aboutsummaryrefslogtreecommitdiff
path: root/mathcomp/ssreflect/Makefile.coq-makefile
diff options
context:
space:
mode:
authorEnrico2018-03-03 10:26:23 +0100
committerGitHub2018-03-03 10:26:23 +0100
commit22692863c2b51cb6b3220e9601d7c237b1830f18 (patch)
tree389049eca835a3ead6c79ca836faf00617e0d91d /mathcomp/ssreflect/Makefile.coq-makefile
parent5811c112c2cf6db25b6a2a1b793d3df5e906b261 (diff)
parentf24095cfbe19c9ddb5ff3dee17a50f715a98acf5 (diff)
Merge pull request #180 from erikmd/export-ssrmatching
Add ssrmatching.v transitional file
Diffstat (limited to 'mathcomp/ssreflect/Makefile.coq-makefile')
-rw-r--r--mathcomp/ssreflect/Makefile.coq-makefile4
1 files changed, 2 insertions, 2 deletions
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 .;\