diff options
Diffstat (limited to 'mathcomp')
| -rw-r--r-- | mathcomp/Makefile | 9 | ||||
| -rw-r--r-- | mathcomp/ssreflect/Makefile | 8 | ||||
| -rw-r--r-- | mathcomp/ssreflect/Makefile.detect-coq-version | 8 |
3 files changed, 0 insertions, 25 deletions
diff --git a/mathcomp/Makefile b/mathcomp/Makefile index c631c7b..f5d495a 100644 --- a/mathcomp/Makefile +++ b/mathcomp/Makefile @@ -6,12 +6,3 @@ COQMAKEOPTIONS=--no-print-directory # Main Makefile include Makefile.common - -# -------------------------------------------------------------------- -# this sets variables COQVERSION and MLLIBEXTRA -# assuming PLUGIN is set to the directory which contains the plugins -# and SSR is set to the directory of the ssreflect package -PLUGIN=../plugin -SSR=ssreflect -include ssreflect/Makefile.detect-coq-version -COQMAKEFILEOPTIONS=$(MLLIBEXTRA) diff --git a/mathcomp/ssreflect/Makefile b/mathcomp/ssreflect/Makefile index 76b8c2c..9d78a7c 100644 --- a/mathcomp/ssreflect/Makefile +++ b/mathcomp/ssreflect/Makefile @@ -6,11 +6,3 @@ COQMAKEOPTIONS=--no-print-directory # Main Makefile include ../Makefile.common - -# -------------------------------------------------------------------- -# this sets variables COQVERSION and MLLIBEXTRA -# assuming PLUGIN is set to the directory which contains the plugins -PLUGIN=../../plugin/ -SSR=. -include Makefile.detect-coq-version -COQMAKEFILEOPTIONS=$(MLLIBEXTRA) diff --git a/mathcomp/ssreflect/Makefile.detect-coq-version b/mathcomp/ssreflect/Makefile.detect-coq-version deleted file mode 100644 index d2e8dce..0000000 --- a/mathcomp/ssreflect/Makefile.detect-coq-version +++ /dev/null @@ -1,8 +0,0 @@ -MLLIBEXTRA=$(shell \ - if [ $(COQVV) = "8.6" ];\ - then cp $(PLUGIN)/v$(COQVV)/ssreflect_plugin.mlpack .;\ - cp $(PLUGIN)/v$(COQVV)/ssreflect.ml4 .;\ - cp $(PLUGIN)/v$(COQVV)/ssrbool.v $(SSR)/;\ - cp $(PLUGIN)/v$(COQVV)/ssrfun.v $(SSR)/;\ - cp $(PLUGIN)/v$(COQVV)/ssreflect.v $(SSR)/;\ - echo "ssreflect_plugin.mlpack ssreflect.ml4"; fi) |