diff options
Diffstat (limited to 'Makefile.build')
-rw-r--r-- | Makefile.build | 20 |
1 files changed, 0 insertions, 20 deletions
diff --git a/Makefile.build b/Makefile.build index cbc1cbaab..2f7ce6ef3 100644 --- a/Makefile.build +++ b/Makefile.build @@ -727,26 +727,6 @@ theories/Init/%.vo theories/Init/%.glob: theories/Init/%.v $(VO_TOOLS_DEP) $(HIDE)rm -f theories/Init/$*.glob $(HIDE)$(BOOTCOQC) $< -noinit -R theories Coq $(TIMING_ARG) $(TIMING_EXTRA) -# MExtraction.v generates the ml core file of the micromega tactic. -# We check that this generated code is still in sync with the version -# of micromega.ml in the archive. - -# Note: we now dump to stdout there via "Recursive Extraction" for better -# control on the name of the generated file, and avoid a .ml that -# would end in our $(MLFILES). The "sed" below is to kill the final -# blank line printed by Recursive Extraction (unlike Extraction "foo"). - -MICROMEGAV:=plugins/micromega/MExtraction.v -MICROMEGAML:=plugins/micromega/micromega.ml -MICROMEGAGEN:=plugins/micromega/.micromega.ml.generated - -$(MICROMEGAV:.v=.vo) $(MICROMEGAV:.v=.glob) : $(MICROMEGAV) theories/Init/Prelude.vo $(VO_TOOLS_DEP) - $(SHOW)'COQC $<' - $(HIDE)rm -f $*.glob - $(HIDE)$(BOOTCOQC) $< | sed -e '$$d' > $(MICROMEGAGEN) - $(HIDE)diff -u --strip-trailing-cr $(MICROMEGAML) $(MICROMEGAGEN) || \ - (2>&1 echo "Error: $(MICROMEGAML) and the code generated by $(MICROMEGAV) differ !" && false) - # The general rule for building .vo files : %.vo %.glob: %.v theories/Init/Prelude.vo $(VO_TOOLS_DEP) |