diff options
| author | letouzey | 2011-03-21 14:41:52 +0000 |
|---|---|---|
| committer | letouzey | 2011-03-21 14:41:52 +0000 |
| commit | 637e67a78096cb59ae309329df7ddc6fc9a6149d (patch) | |
| tree | bddab672876de2b6cb414d7ed1e32e4f1bcee8af | |
| parent | ed9bc81551eb8cf9e51d3824add3fa0b5b6c88a9 (diff) | |
Makefile.build: states/initial.coq was wrongly done with -dont-load-proofs
This was breaking the FireSquad extraction test
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13919 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | Makefile.build | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/Makefile.build b/Makefile.build index d97b8e0975..529238d674 100644 --- a/Makefile.build +++ b/Makefile.build @@ -75,8 +75,9 @@ TIMECMD= # is "'time -p'" to get compilation time of .v LOADPROOFS=-dont-load-proofs -COQOPTS=$(COQ_XML) $(VM) $(LOADPROOFS) +COQOPTS=$(COQ_XML) $(VM) BOOTCOQTOP:=$(TIMECMD) $(BESTCOQTOP) -boot $(COQOPTS) +BOOTCOQC:=$(BOOTCOQTOP) $(LOADPROOFS) -compile # The SHOW and HIDE variables control whether make will echo complete commands # or only abbreviated versions. @@ -467,7 +468,7 @@ states/initial.coq: states/MakeInitial.v $(INITVO) $(VO_TOOLS_STRICT) | states/M theories/Init/%.vo theories/Init/%.glob: theories/Init/%.v $(VO_TOOLS_STRICT) | theories/Init/%.v.d $(VO_TOOLS_ORDER_ONLY) $(SHOW)'COQC -nois $<' $(HIDE)rm -f theories/Init/$*.glob - $(HIDE)$(BOOTCOQTOP) -nois -compile theories/Init/$* + $(HIDE)$(BOOTCOQC) theories/Init/$* -nois theories/Numbers/Natural/BigN/NMake_gen.v: theories/Numbers/Natural/BigN/NMake_gen.ml $(OCAML) $< $(TOTARGET) @@ -848,7 +849,7 @@ plugins/%_mod.ml: plugins/%.mllib %.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 $* + $(HIDE)$(BOOTCOQC) $* ifdef VALIDATE $(SHOW)'COQCHK $(call vo_to_mod,$@)' $(HIDE)$(BESTCHICKEN) -boot -silent -norec $(call vo_to_mod,$@) \ |