aboutsummaryrefslogtreecommitdiffhomepage
path: root/Makefile.build
diff options
context:
space:
mode:
Diffstat (limited to 'Makefile.build')
-rw-r--r--Makefile.build4
1 files changed, 2 insertions, 2 deletions
diff --git a/Makefile.build b/Makefile.build
index a87d0032b..e91ffb86a 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -563,7 +563,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) -dump-glob theories/Init/$*.glob -nois -compile theories/Init/$*
+ $(HIDE)$(BOOTCOQTOP) -nois -compile theories/Init/$*
theories/Numbers/Natural/BigN/NMake.v: theories/Numbers/Natural/BigN/NMake_gen.ml
$(OCAML) $< > $@
@@ -875,7 +875,7 @@ endif
%.vo %.glob: %.v states/initial.coq $(VO_TOOLS_STRICT) | %.v.d $(VO_TOOLS_ORDER_ONLY)
$(SHOW)'COQC $<'
$(HIDE)rm -f $*.glob
- $(HIDE)$(BOOTCOQTOP) -dump-glob $*.glob -compile $*
+ $(HIDE)$(BOOTCOQTOP) -compile $*
ifdef VALIDATE
$(SHOW)'COQCHK $(shell basename $*)'
$(HIDE)$(BESTCHICKEN) -silent -norec $(shell basename $*) \