Merge PR #6234: Make the micromega extraction check a regular output test.

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)