diff options
| author | Cyril Cohen | 2018-07-31 16:17:07 +0200 |
|---|---|---|
| committer | Cyril Cohen | 2018-07-31 16:17:07 +0200 |
| commit | 629a7a065146679f14f95abf1de63a7ff3a2eacc (patch) | |
| tree | e78cba9b79b6f509a37d645a95139d143add6632 | |
| parent | 5892b9b06ec9cd16584c4c56884949c23949cffe (diff) | |
agressive fix for duplicated files!
| -rw-r--r-- | mathcomp/Makefile | 4 | ||||
| -rw-r--r-- | mathcomp/ssreflect/Makefile | 9 | ||||
| -rw-r--r-- | mathcomp/ssreflect/Makefile.detect-coq-version | 10 | ||||
| -rw-r--r-- | plugin/v8.6/ssrbool.v (renamed from mathcomp/ssreflect/plugin/v8.6/ssrbool.v) | 0 | ||||
| -rw-r--r-- | plugin/v8.6/ssreflect.ml4 (renamed from mathcomp/ssreflect/plugin/v8.6/ssreflect.ml4) | 0 | ||||
| -rw-r--r-- | plugin/v8.6/ssreflect.v (renamed from mathcomp/ssreflect/plugin/v8.6/ssreflect.v) | 0 | ||||
| -rw-r--r-- | plugin/v8.6/ssreflect_plugin.mlpack (renamed from mathcomp/ssreflect/plugin/v8.6/ssreflect_plugin.mlpack) | 0 | ||||
| -rw-r--r-- | plugin/v8.6/ssrfun.v (renamed from mathcomp/ssreflect/plugin/v8.6/ssrfun.v) | 0 |
8 files changed, 11 insertions, 12 deletions
diff --git a/mathcomp/Makefile b/mathcomp/Makefile index 2acfa83..9064020 100644 --- a/mathcomp/Makefile +++ b/mathcomp/Makefile @@ -9,7 +9,9 @@ include Makefile.common # -------------------------------------------------------------------- # this sets variable V (coq version) and MLLIBEXTRA -# assuming SSR is set to the directory which contains the ssreflect package +# 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 8587073..c3092fc 100644 --- a/mathcomp/ssreflect/Makefile +++ b/mathcomp/ssreflect/Makefile @@ -2,8 +2,6 @@ # setting variables COQPROJECT?=Make -BEFOREMAKEFILES+=Makefile.coqdep -OTHERCLEAN+=Makefile.coqdep COQMAKEOPTIONS=--no-print-directory # Main Makefile @@ -11,10 +9,9 @@ include ../Makefile.common # -------------------------------------------------------------------- # this sets variable V (coq version) and MLLIBEXTRA -# assuming SSR is set to the directory which contains the ssreflect package +# assuming PLUGIN is set to the directory which contains the plugins +PLUGIN=../../plugin/ SSR=. include Makefile.detect-coq-version -COQMAKEFILEOPTIONS=$(MLLIBEXTRA) -Makefile.coqdep: - echo "COQDEP=$(COQDEP) -exclude-dir ssreflect/plugin -c" > Makefile.coqdep +COQMAKEFILEOPTIONS=$(MLLIBEXTRA) diff --git a/mathcomp/ssreflect/Makefile.detect-coq-version b/mathcomp/ssreflect/Makefile.detect-coq-version index 385c078..0f7d9de 100644 --- a/mathcomp/ssreflect/Makefile.detect-coq-version +++ b/mathcomp/ssreflect/Makefile.detect-coq-version @@ -12,9 +12,9 @@ V:=$(BRANCH_coq) MLLIBEXTRA:=$(shell \ if [ $(V) = "8.6" ];\ - then cp $(SSR)/plugin/v$(V)/ssreflect_plugin.mlpack .;\ - cp $(SSR)/plugin/v$(V)/ssreflect.ml4 .;\ - cp $(SSR)/plugin/v$(V)/ssrbool.v $(SSR)/;\ - cp $(SSR)/plugin/v$(V)/ssrfun.v $(SSR)/;\ - cp $(SSR)/plugin/v$(V)/ssreflect.v $(SSR)/;\ + then cp $(PLUGIN)/v$(V)/ssreflect_plugin.mlpack .;\ + cp $(PLUGIN)/v$(V)/ssreflect.ml4 .;\ + cp $(PLUGIN)/v$(V)/ssrbool.v $(SSR)/;\ + cp $(PLUGIN)/v$(V)/ssrfun.v $(SSR)/;\ + cp $(PLUGIN)/v$(V)/ssreflect.v $(SSR)/;\ echo "ssreflect_plugin.mlpack ssreflect.ml4"; fi) diff --git a/mathcomp/ssreflect/plugin/v8.6/ssrbool.v b/plugin/v8.6/ssrbool.v index 2342ec6..2342ec6 100644 --- a/mathcomp/ssreflect/plugin/v8.6/ssrbool.v +++ b/plugin/v8.6/ssrbool.v diff --git a/mathcomp/ssreflect/plugin/v8.6/ssreflect.ml4 b/plugin/v8.6/ssreflect.ml4 index 25d3287..25d3287 100644 --- a/mathcomp/ssreflect/plugin/v8.6/ssreflect.ml4 +++ b/plugin/v8.6/ssreflect.ml4 diff --git a/mathcomp/ssreflect/plugin/v8.6/ssreflect.v b/plugin/v8.6/ssreflect.v index e63b45b..e63b45b 100644 --- a/mathcomp/ssreflect/plugin/v8.6/ssreflect.v +++ b/plugin/v8.6/ssreflect.v diff --git a/mathcomp/ssreflect/plugin/v8.6/ssreflect_plugin.mlpack b/plugin/v8.6/ssreflect_plugin.mlpack index 006b70f..006b70f 100644 --- a/mathcomp/ssreflect/plugin/v8.6/ssreflect_plugin.mlpack +++ b/plugin/v8.6/ssreflect_plugin.mlpack diff --git a/mathcomp/ssreflect/plugin/v8.6/ssrfun.v b/plugin/v8.6/ssrfun.v index 7cb30ff..7cb30ff 100644 --- a/mathcomp/ssreflect/plugin/v8.6/ssrfun.v +++ b/plugin/v8.6/ssrfun.v |