aboutsummaryrefslogtreecommitdiffhomepage
path: root/Makefile.build
diff options
context:
space:
mode:
Diffstat (limited to 'Makefile.build')
-rw-r--r--Makefile.build5
1 files changed, 2 insertions, 3 deletions
diff --git a/Makefile.build b/Makefile.build
index bc89d6b99..ffac80cb8 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -556,7 +556,6 @@ program: $(PROGRAMVO)
structures: $(STRUCTURESVO)
vectors: $(VECTORSVO)
msets: $(MSETSVO)
-mmaps: $(MMAPSVO)
compat: $(COMPATVO)
noreal: unicode logic arith bool zarith qarith lists sets fsets \
@@ -589,9 +588,9 @@ pluginsbyte: $(PLUGINS)
###########################################################################
theories/Init/%.vo theories/Init/%.glob: theories/Init/%.v $(VO_TOOLS_DEP) | theories/Init/%.v.d
- $(SHOW)'COQC -noinit $<'
+ $(SHOW)'COQC $(COQ_XML) -noinit $<'
$(HIDE)rm -f theories/Init/$*.glob
- $(HIDE)$(BOOTCOQC) $< -noinit -R theories Coq
+ $(HIDE)$(BOOTCOQC) $< $(COQ_XML) -noinit -R theories Coq
theories/Numbers/Natural/BigN/NMake_gen.v: theories/Numbers/Natural/BigN/NMake_gen.ml
$(OCAML) $< $(TOTARGET)