diff options
| -rw-r--r-- | Makefile | 2 | ||||
| -rw-r--r-- | Makefile.build | 2 | ||||
| -rw-r--r-- | Makefile.common | 6 |
3 files changed, 8 insertions, 2 deletions
@@ -88,7 +88,7 @@ export GENMLFILES:=$(LEXFILES:.mll=.ml) $(YACCFILES:.mly=.ml) \ scripts/tolink.ml kernel/copcodes.ml export GENMLIFILES:=$(YACCFILES:.mly=.mli) export GENHFILES:=kernel/byterun/coq_jumptbl.h -export GENVFILES:=theories/Numbers/Natural/BigN/NMake.v +export GENVFILES:=theories/Numbers/Natural/BigN/NMake_gen.v export GENFILES:=$(GENMLFILES) $(GENMLIFILES) $(GENHFILES) $(GENVFILES) export MLFILES := $(shell find . $(FIND_VCS_CLAUSE) '(' -name '*.ml' ')' $(FIND_PRINTF_P) | \ while read f; do if ! [ -e "$${f}4" ]; then echo "$$f"; fi; done) \ diff --git a/Makefile.build b/Makefile.build index 864f6f27b..7d63e33b0 100644 --- a/Makefile.build +++ b/Makefile.build @@ -796,7 +796,7 @@ plugins/%_mod.ml: plugins/%.mllib $(HIDE)$(CAMLP4O) $(CAMLP4EXTENDFLAGS) pr_o.cmo `$(CAMLP4USE) $<` `$(CAMLP4DEPS) $<` $(CAMLP4COMPAT) -impl $< > $@ \ || ( RV=$$?; rm -f "$@"; exit $${RV} ) -%.vo %.glob: %.v states/initial.coq $(VO_TOOLS_STRICT) | %.v.d $(VO_TOOLS_ORDER_ONLY) +%.vo %.glob: %.v states/initial.coq $(INITPLUGINSBEST) $(VO_TOOLS_STRICT) | %.v.d $(VO_TOOLS_ORDER_ONLY) $(SHOW)'COQC $<' $(HIDE)rm -f $*.glob $(HIDE)$(BOOTCOQTOP) -compile $* diff --git a/Makefile.common b/Makefile.common index a1bfd0885..de84aaefe 100644 --- a/Makefile.common +++ b/Makefile.common @@ -204,6 +204,12 @@ else PLUGINSOPT:= endif +ifeq ($(BEST),opt) + INITPLUGINSBEST:=$(INITPLUGINSOPT) +else + INITPLUGINSBEST:=$(INITPLUGINS) +endif + CMA:=$(CLIBS) $(CAMLP4OBJS) CMXA:=$(CMA:.cma=.cmxa) |