diff options
| author | Erik Martin-Dorel | 2018-02-25 23:56:29 +0100 |
|---|---|---|
| committer | Erik Martin-Dorel | 2018-02-26 15:23:18 +0100 |
| commit | f24095cfbe19c9ddb5ff3dee17a50f715a98acf5 (patch) | |
| tree | 44c34baf4012a9eeda9ad68476ce72ec7cf00ce8 /mathcomp/ssreflect/Makefile.coq-makefile | |
| parent | 13f26ccc09f87b222f9601892f085276a6ddb8c0 (diff) | |
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
Diffstat (limited to 'mathcomp/ssreflect/Makefile.coq-makefile')
| -rw-r--r-- | mathcomp/ssreflect/Makefile.coq-makefile | 4 |
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 .;\ |