1 files changed, 0 insertions, 109 deletions
diff --git a/contrib/extraction/test/Makefile b/contrib/extraction/test/Makefile
deleted file mode 100644
index 65a54090..00000000
--- a/contrib/extraction/test/Makefile
+++ /dev/null
@@ -1,109 +0,0 @@
-# 
-#	General variables
-#
-
-TOPDIR=../../..
-
-# Files with axioms to be realized: can't be extracted directly
-
-AXIOMSVO:= \
-theories/Reals/% \
-theories/Num/%
-
-DIRS:= $(shell (cd $(TOPDIR);find theories -type d ! -path \*.svn\*))
-
-INCL:= $(patsubst %,-I %,$(DIRS))
-
-VO:= $(shell (cd $(TOPDIR);find theories -name \*.vo))
-
-VO:= $(filter-out $(AXIOMSVO),$(VO))
-
-ML:= $(shell test -x v2ml && ./v2ml $(VO))
-
-MLI:= $(patsubst %.ml,%.mli,$(ML))
-
-CMO:= $(patsubst %.ml,%.cmo,$(ML))
-
-OSTDLIB:=$(shell (ocamlc -where))
-
-#
-#	General rules 
-#
-
-all: v2ml ml $(MLI) $(CMO)
-
-ml: $(ML)
-
-depend: #$(ML)
-	rm -f .depend; ocamldep $(INCL) theories/*/*.ml theories/*/*.mli > .depend
-
-tree:
-	mkdir -p $(DIRS)
-	cp $(OSTDLIB)/pervasives.cmi $(OSTDLIB)/obj.cmi $(OSTDLIB)/lazy.cmi theories
-
-#%.mli:%.ml
-#	./make_mli $< > $@
-
-%.cmi:%.mli
-	ocamlc -c $(INCL) -nostdlib $<
-
-%.cmo:%.ml
-	ocamlc -c $(INCL) -nostdlib $<
-
-$(ML): ml2v
-	./extract $@
-
-clean: 
-	rm -f theories/*/*.ml* theories/*/*.cm*
-
-
-#
-#	Utilities
-#
-
-open: 
-	find theories -name "*".ml -exec ./qualify2open \{\} \;
-
-undo_open: 
-	find theories -name "*".ml -exec mv \{\}.orig \{\} \;
-
-ml2v: ml2v.ml
-	ocamlopt -o $@ $<
-
-v2ml: v2ml.ml
-	ocamlopt -o $@ $< 
-	$(MAKE)
-
-#
-#	Extraction of Reals
-#
-
-
-REALSAXIOMSVO:=theories/Reals/Rsyntax.vo
-
-REALSALLVO:=$(shell cd $(TOPDIR); ls -tr theories/Reals/*.vo)
-REALSVO:=$(filter-out $(REALSAXIOMSVO),$(REALSALLVO))
-REALSML:=$(shell test -x v2ml && ./v2ml $(REALSVO))
-REALSCMO:= $(patsubst %.ml,%.cmo,$(REALSML))
-
-reals: all realsml theories/Reals/addReals.cmo $(REALSCMO)
-
-realsml: $(REALSML)
-
-theories/Reals/addReals.ml: 
-	cp -f addReals theories/Reals/addReals.ml
-
-$(REALSML): 
-	./extract $@
-
-
-#
-#	The End
-#
-
-.PHONY: all tree clean reals realsml depend
-
-include .depend
-
-
-