diff options
| author | Enrico Tassi | 2017-06-09 15:41:09 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2017-06-09 15:41:09 +0200 |
| commit | 4f6362b1b783b296f58c7dff293f68c02d015ea5 (patch) | |
| tree | 20182f0a7d847646f76fa96ee58d2ec8d2213453 /mathcomp/ssreflect/Makefile.coq-makefile | |
| parent | fd641345d0678660e60a3d81676e05e0c6d15a90 (diff) | |
fix compilation on 8.5
Diffstat (limited to 'mathcomp/ssreflect/Makefile.coq-makefile')
| -rw-r--r-- | mathcomp/ssreflect/Makefile.coq-makefile | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/mathcomp/ssreflect/Makefile.coq-makefile b/mathcomp/ssreflect/Makefile.coq-makefile index 144f6e4..68bfbc2 100644 --- a/mathcomp/ssreflect/Makefile.coq-makefile +++ b/mathcomp/ssreflect/Makefile.coq-makefile @@ -9,9 +9,12 @@ define coqmakefile $$LN $(1)/plugin/$(V)/ssrmatching.ml4 .;\ $$LN $(1)/plugin/$(V)/ssrmatching.v .;\ $$LN $(1)/plugin/$(V)/ssreflect_plugin.mllib .;\ - EXTRA="ssrmatching.mli ssrmatching.ml4 ssrmatching.v ssreflect.ml4";\ - MLLIB=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=ssreflect_plugin.mllib;\ + EXTRA="ssrmatching.mli ssrmatching.ml4 ssrmatching.v ssreflect.ml4";\ ;;\ v8.6*)\ $$LN $(1)/plugin/$(V)/ssreflect_plugin.mlpack .;\ |