suite et fin (?) de haskell: gestion des modules, mise en place du'un test

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2480 85f007b7-540e-0410-9357-904b9bb8a0f7

6 files changed, 422 insertions, 2 deletions

diff --git a/contrib/extraction/test/.cvsignore b/contrib/extraction/test/.cvsignore
index 087fa7d9d..fa307db73 100644
--- a/contrib/extraction/test/.cvsignore
+++ b/contrib/extraction/test/.cvsignore
@@ -1,6 +1,7 @@
 theories
 ml2v 
 v2ml
+hs2v
+v2hs
 log
-
-*.h*
+*.hi
diff --git a/contrib/extraction/test/Makefile.haskell b/contrib/extraction/test/Makefile.haskell
new file mode 100644
index 000000000..8dc8d0166
--- /dev/null
+++ b/contrib/extraction/test/Makefile.haskell
@@ -0,0 +1,378 @@
+# 
+#	General variables
+#
+
+TOPDIR=../../..
+
+# Files with axioms to be realized: can't be extracted directly
+
+AXIOMSVO:= \
+theories/Init/Prelude.vo \
+theories/Arith/Arith.vo \
+theories/Lists/List.vo \
+theories/Reals/% \
+theories/Reals/Rsyntax.vo \
+theories/Num/% \
+theories/ZArith/Zsyntax.vo
+
+DIRS:= $(shell (cd $(TOPDIR);find theories -type d ! -name CVS))
+
+INCL:= $(patsubst %,-i%,$(DIRS))
+
+VO:= $(shell (cd $(TOPDIR);find theories -name \*.vo))
+
+VO:= $(filter-out $(AXIOMSVO),$(VO))
+
+HS:= $(shell test -x v2hs && ./v2hs $(VO))
+
+O:= $(patsubst %.hs,%.o,$(HS))
+
+#
+#	General rules 
+#
+
+all: v2hs hs Unit.o $(O)
+
+hs: $(HS)
+
+tree:
+	mkdir -p $(DIRS)
+
+%.o:%.hs
+	hbc $(INCL) -c $<
+
+$(HS): hs2v
+	./extract.haskell $@
+
+clean: 
+	rm -f theories/*/*.*
+
+
+#
+#	Utilities
+#
+
+hs2v: hs2v.ml
+	ocamlc -o $@ $<
+
+v2hs: v2hs.ml
+	ocamlc -o $@ $< 
+	$(MAKE) -f Makefile.haskell
+
+
+#
+#	The End
+#
+
+.PHONY: all tree clean depend
+
+# DO NOT DELETE: Beginning of Haskell dependencies
+theories/Arith/Between.o : theories/Arith/Between.hs
+theories/Arith/Compare.o : theories/Arith/Compare.hs
+theories/Arith/Compare.o : theories/Arith/Compare_dec.o
+theories/Arith/Compare.o : theories/Init/Specif.o
+theories/Arith/Compare_dec.o : theories/Arith/Compare_dec.hs
+theories/Arith/Compare_dec.o : theories/Init/Datatypes.o
+theories/Arith/Compare_dec.o : theories/Init/Logic.o
+theories/Arith/Compare_dec.o : theories/Init/Specif.o
+theories/Arith/Div2.o : theories/Arith/Div2.hs
+theories/Arith/Div2.o : theories/Init/Datatypes.o
+theories/Arith/Div2.o : theories/Init/Peano.o
+theories/Arith/EqNat.o : theories/Arith/EqNat.hs
+theories/Arith/EqNat.o : theories/Init/Datatypes.o
+theories/Arith/EqNat.o : theories/Init/Specif.o
+theories/Arith/Euclid.o : theories/Arith/Compare_dec.o
+theories/Arith/Euclid.o : theories/Arith/Euclid.hs
+theories/Arith/Euclid.o : theories/Arith/Minus.o
+theories/Arith/Euclid.o : theories/Arith/Wf_nat.o
+theories/Arith/Euclid.o : theories/Init/Datatypes.o
+theories/Arith/Euclid.o : theories/Init/Specif.o
+theories/Arith/Even.o : theories/Arith/Even.hs
+theories/Arith/Even.o : theories/Init/Datatypes.o
+theories/Arith/Even.o : theories/Init/Specif.o
+theories/Arith/Gt.o : theories/Arith/Gt.hs
+theories/Arith/Le.o : theories/Arith/Le.hs
+theories/Arith/Lt.o : theories/Arith/Lt.hs
+theories/Arith/Max.o : theories/Arith/Max.hs
+theories/Arith/Max.o : theories/Init/Datatypes.o
+theories/Arith/Max.o : theories/Init/Logic.o
+theories/Arith/Max.o : theories/Init/Specif.o
+theories/Arith/Min.o : theories/Arith/Min.hs
+theories/Arith/Min.o : theories/Init/Datatypes.o
+theories/Arith/Min.o : theories/Init/Logic.o
+theories/Arith/Min.o : theories/Init/Specif.o
+theories/Arith/Minus.o : theories/Arith/Minus.hs
+theories/Arith/Minus.o : theories/Init/Datatypes.o
+theories/Arith/Mult.o : theories/Arith/Mult.hs
+theories/Arith/Mult.o : theories/Arith/Plus.o
+theories/Arith/Mult.o : theories/Init/Datatypes.o
+theories/Arith/Peano_dec.o : theories/Arith/Peano_dec.hs
+theories/Arith/Peano_dec.o : theories/Init/Datatypes.o
+theories/Arith/Peano_dec.o : theories/Init/Specif.o
+theories/Arith/Plus.o : theories/Arith/Plus.hs
+theories/Arith/Plus.o : theories/Init/Datatypes.o
+theories/Arith/Plus.o : theories/Init/Logic.o
+theories/Arith/Plus.o : theories/Init/Specif.o
+theories/Arith/Wf_nat.o : theories/Arith/Wf_nat.hs
+theories/Arith/Wf_nat.o : theories/Init/Datatypes.o
+theories/Arith/Wf_nat.o : theories/Init/Logic.o
+theories/Arith/Wf_nat.o : theories/Init/Wf.o
+theories/Bool/Bool.o : theories/Bool/Bool.hs
+theories/Bool/Bool.o : theories/Init/Datatypes.o
+theories/Bool/Bool.o : theories/Init/Specif.o
+theories/Bool/BoolEq.o : theories/Bool/BoolEq.hs
+theories/Bool/BoolEq.o : theories/Init/Datatypes.o
+theories/Bool/BoolEq.o : theories/Init/Specif.o
+theories/Bool/DecBool.o : theories/Bool/DecBool.hs
+theories/Bool/DecBool.o : theories/Init/Specif.o
+theories/Bool/IfProp.o : theories/Bool/IfProp.hs
+theories/Bool/IfProp.o : theories/Init/Datatypes.o
+theories/Bool/IfProp.o : theories/Init/Specif.o
+theories/Bool/Sumbool.o : theories/Bool/Sumbool.hs
+theories/Bool/Sumbool.o : theories/Init/Datatypes.o
+theories/Bool/Sumbool.o : theories/Init/Specif.o
+theories/Bool/Zerob.o : theories/Bool/Zerob.hs
+theories/Bool/Zerob.o : theories/Init/Datatypes.o
+theories/Init/Datatypes.o : theories/Init/Datatypes.hs
+theories/Init/DatatypesSyntax.o : theories/Init/DatatypesSyntax.hs
+theories/Init/Logic.o : theories/Init/Logic.hs
+theories/Init/LogicSyntax.o : theories/Init/LogicSyntax.hs
+theories/Init/Logic_Type.o : theories/Init/Logic_Type.hs
+theories/Init/Logic_TypeSyntax.o : theories/Init/Logic_TypeSyntax.hs
+theories/Init/Peano.o : theories/Init/Datatypes.o
+theories/Init/Peano.o : theories/Init/Peano.hs
+theories/Init/Specif.o : theories/Init/Datatypes.o
+theories/Init/Specif.o : theories/Init/Logic.o
+theories/Init/Specif.o : theories/Init/Specif.hs
+theories/Init/SpecifSyntax.o : theories/Init/SpecifSyntax.hs
+theories/Init/Wf.o : theories/Init/Wf.hs
+theories/IntMap/Adalloc.o : theories/Bool/Sumbool.o
+theories/IntMap/Adalloc.o : theories/Init/Datatypes.o
+theories/IntMap/Adalloc.o : theories/Init/Logic.o
+theories/IntMap/Adalloc.o : theories/Init/Specif.o
+theories/IntMap/Adalloc.o : theories/IntMap/Adalloc.hs
+theories/IntMap/Adalloc.o : theories/IntMap/Addec.o
+theories/IntMap/Adalloc.o : theories/IntMap/Addr.o
+theories/IntMap/Adalloc.o : theories/IntMap/Map.o
+theories/IntMap/Adalloc.o : theories/ZArith/Fast_integer.o
+theories/IntMap/Addec.o : theories/Bool/Sumbool.o
+theories/IntMap/Addec.o : theories/Init/Datatypes.o
+theories/IntMap/Addec.o : theories/Init/Specif.o
+theories/IntMap/Addec.o : theories/IntMap/Addec.hs
+theories/IntMap/Addec.o : theories/IntMap/Addr.o
+theories/IntMap/Addec.o : theories/ZArith/Fast_integer.o
+theories/IntMap/Addr.o : theories/Bool/Bool.o
+theories/IntMap/Addr.o : theories/Init/Datatypes.o
+theories/IntMap/Addr.o : theories/Init/Specif.o
+theories/IntMap/Addr.o : theories/IntMap/Addr.hs
+theories/IntMap/Addr.o : theories/ZArith/Fast_integer.o
+theories/IntMap/Adist.o : theories/Arith/Min.o
+theories/IntMap/Adist.o : theories/Init/Datatypes.o
+theories/IntMap/Adist.o : theories/IntMap/Addr.o
+theories/IntMap/Adist.o : theories/IntMap/Adist.hs
+theories/IntMap/Adist.o : theories/ZArith/Fast_integer.o
+theories/IntMap/Allmaps.o : theories/IntMap/Allmaps.hs
+theories/IntMap/Fset.o : theories/Init/Datatypes.o
+theories/IntMap/Fset.o : theories/Init/Logic.o
+theories/IntMap/Fset.o : theories/Init/Specif.o
+theories/IntMap/Fset.o : theories/IntMap/Addec.o
+theories/IntMap/Fset.o : theories/IntMap/Addr.o
+theories/IntMap/Fset.o : theories/IntMap/Fset.hs
+theories/IntMap/Fset.o : theories/IntMap/Map.o
+theories/IntMap/Lsort.o : theories/Bool/Bool.o
+theories/IntMap/Lsort.o : theories/Bool/Sumbool.o
+theories/IntMap/Lsort.o : theories/Init/Datatypes.o
+theories/IntMap/Lsort.o : theories/Init/Logic.o
+theories/IntMap/Lsort.o : theories/Init/Specif.o
+theories/IntMap/Lsort.o : theories/IntMap/Addec.o
+theories/IntMap/Lsort.o : theories/IntMap/Addr.o
+theories/IntMap/Lsort.o : theories/IntMap/Lsort.hs
+theories/IntMap/Lsort.o : theories/IntMap/Mapiter.o
+theories/IntMap/Lsort.o : theories/Lists/PolyList.o
+theories/IntMap/Lsort.o : theories/ZArith/Fast_integer.o
+theories/IntMap/Map.o : theories/Init/Datatypes.o
+theories/IntMap/Map.o : theories/Init/Peano.o
+theories/IntMap/Map.o : theories/Init/Specif.o
+theories/IntMap/Map.o : theories/IntMap/Addec.o
+theories/IntMap/Map.o : theories/IntMap/Addr.o
+theories/IntMap/Map.o : theories/IntMap/Map.hs
+theories/IntMap/Map.o : theories/ZArith/Fast_integer.o
+theories/IntMap/Mapaxioms.o : theories/IntMap/Mapaxioms.hs
+theories/IntMap/Mapc.o : theories/IntMap/Mapc.hs
+theories/IntMap/Mapcanon.o : theories/IntMap/Map.o
+theories/IntMap/Mapcanon.o : theories/IntMap/Mapcanon.hs
+theories/IntMap/Mapcard.o : theories/Arith/Peano_dec.o
+theories/IntMap/Mapcard.o : theories/Arith/Plus.o
+theories/IntMap/Mapcard.o : theories/Bool/Sumbool.o
+theories/IntMap/Mapcard.o : theories/Init/Datatypes.o
+theories/IntMap/Mapcard.o : theories/Init/Logic.o
+theories/IntMap/Mapcard.o : theories/Init/Peano.o
+theories/IntMap/Mapcard.o : theories/Init/Specif.o
+theories/IntMap/Mapcard.o : theories/IntMap/Addec.o
+theories/IntMap/Mapcard.o : theories/IntMap/Addr.o
+theories/IntMap/Mapcard.o : theories/IntMap/Map.o
+theories/IntMap/Mapcard.o : theories/IntMap/Mapcard.hs
+theories/IntMap/Mapfold.o : theories/Init/Datatypes.o
+theories/IntMap/Mapfold.o : theories/Init/Logic.o
+theories/IntMap/Mapfold.o : theories/Init/Specif.o
+theories/IntMap/Mapfold.o : theories/IntMap/Fset.o
+theories/IntMap/Mapfold.o : theories/IntMap/Map.o
+theories/IntMap/Mapfold.o : theories/IntMap/Mapfold.hs
+theories/IntMap/Mapfold.o : theories/IntMap/Mapiter.o
+theories/IntMap/Mapiter.o : theories/Bool/Sumbool.o
+theories/IntMap/Mapiter.o : theories/Init/Datatypes.o
+theories/IntMap/Mapiter.o : theories/Init/Logic.o
+theories/IntMap/Mapiter.o : theories/Init/Specif.o
+theories/IntMap/Mapiter.o : theories/IntMap/Addec.o
+theories/IntMap/Mapiter.o : theories/IntMap/Addr.o
+theories/IntMap/Mapiter.o : theories/IntMap/Map.o
+theories/IntMap/Mapiter.o : theories/IntMap/Mapiter.hs
+theories/IntMap/Mapiter.o : theories/Lists/PolyList.o
+theories/IntMap/Maplists.o : theories/Bool/Bool.o
+theories/IntMap/Maplists.o : theories/Bool/Sumbool.o
+theories/IntMap/Maplists.o : theories/Init/Datatypes.o
+theories/IntMap/Maplists.o : theories/Init/Logic.o
+theories/IntMap/Maplists.o : theories/Init/Specif.o
+theories/IntMap/Maplists.o : theories/IntMap/Addec.o
+theories/IntMap/Maplists.o : theories/IntMap/Map.o
+theories/IntMap/Maplists.o : theories/IntMap/Mapiter.o
+theories/IntMap/Maplists.o : theories/IntMap/Maplists.hs
+theories/IntMap/Maplists.o : theories/Lists/PolyList.o
+theories/IntMap/Mapsubset.o : theories/Bool/Bool.o
+theories/IntMap/Mapsubset.o : theories/Init/Datatypes.o
+theories/IntMap/Mapsubset.o : theories/IntMap/Fset.o
+theories/IntMap/Mapsubset.o : theories/IntMap/Map.o
+theories/IntMap/Mapsubset.o : theories/IntMap/Mapiter.o
+theories/IntMap/Mapsubset.o : theories/IntMap/Mapsubset.hs
+theories/Lists/ListSet.o : theories/Init/Datatypes.o
+theories/Lists/ListSet.o : theories/Init/Logic.o
+theories/Lists/ListSet.o : theories/Init/Specif.o
+theories/Lists/ListSet.o : theories/Lists/ListSet.hs
+theories/Lists/ListSet.o : theories/Lists/PolyList.o
+theories/Lists/PolyList.o : theories/Init/Datatypes.o
+theories/Lists/PolyList.o : theories/Init/Specif.o
+theories/Lists/PolyList.o : theories/Lists/PolyList.hs
+theories/Lists/PolyListSyntax.o : theories/Lists/PolyListSyntax.hs
+theories/Lists/Streams.o : theories/Init/Datatypes.o
+theories/Lists/Streams.o : theories/Lists/Streams.hs
+theories/Lists/TheoryList.o : theories/Bool/DecBool.o
+theories/Lists/TheoryList.o : theories/Init/Datatypes.o
+theories/Lists/TheoryList.o : theories/Init/Specif.o
+theories/Lists/TheoryList.o : theories/Lists/PolyList.o
+theories/Lists/TheoryList.o : theories/Lists/TheoryList.hs
+theories/Logic/Berardi.o : theories/Logic/Berardi.hs
+theories/Logic/Classical.o : theories/Logic/Classical.hs
+theories/Logic/Classical_Pred_Set.o : theories/Logic/Classical_Pred_Set.hs
+theories/Logic/Classical_Pred_Type.o : theories/Logic/Classical_Pred_Type.hs
+theories/Logic/Classical_Prop.o : theories/Logic/Classical_Prop.hs
+theories/Logic/Classical_Type.o : theories/Logic/Classical_Type.hs
+theories/Logic/Decidable.o : theories/Logic/Decidable.hs
+theories/Logic/Elimdep.o : theories/Logic/Elimdep.hs
+theories/Logic/Eqdep.o : theories/Logic/Eqdep.hs
+theories/Logic/Eqdep_dec.o : theories/Logic/Eqdep_dec.hs
+theories/Logic/JMeq.o : theories/Logic/JMeq.hs
+theories/Relations/Newman.o : theories/Relations/Newman.hs
+theories/Relations/Operators_Properties.o : theories/Relations/Operators_Properties.hs
+theories/Relations/Relation_Definitions.o : theories/Relations/Relation_Definitions.hs
+theories/Relations/Relation_Operators.o : theories/Relations/Relation_Operators.hs
+theories/Relations/Relations.o : theories/Relations/Relations.hs
+theories/Relations/Rstar.o : theories/Relations/Rstar.hs
+theories/Setoids/Setoid.o : theories/Setoids/Setoid.hs
+theories/Sets/Classical_sets.o : theories/Sets/Classical_sets.hs
+theories/Sets/Constructive_sets.o : theories/Sets/Constructive_sets.hs
+theories/Sets/Cpo.o : theories/Sets/Cpo.hs
+theories/Sets/Ensembles.o : theories/Sets/Ensembles.hs
+theories/Sets/Finite_sets.o : theories/Sets/Finite_sets.hs
+theories/Sets/Finite_sets_facts.o : theories/Sets/Finite_sets_facts.hs
+theories/Sets/Image.o : theories/Sets/Image.hs
+theories/Sets/Infinite_sets.o : theories/Sets/Infinite_sets.hs
+theories/Sets/Integers.o : theories/Sets/Integers.hs
+theories/Sets/Integers.o : theories/Sets/Partial_Order.o
+theories/Sets/Multiset.o : theories/Init/Datatypes.o
+theories/Sets/Multiset.o : theories/Init/Peano.o
+theories/Sets/Multiset.o : theories/Init/Specif.o
+theories/Sets/Multiset.o : theories/Sets/Multiset.hs
+theories/Sets/Partial_Order.o : theories/Sets/Partial_Order.hs
+theories/Sets/Permut.o : theories/Sets/Permut.hs
+theories/Sets/Powerset.o : theories/Sets/Partial_Order.o
+theories/Sets/Powerset.o : theories/Sets/Powerset.hs
+theories/Sets/Powerset_Classical_facts.o : theories/Sets/Powerset_Classical_facts.hs
+theories/Sets/Powerset_facts.o : theories/Sets/Powerset_facts.hs
+theories/Sets/Relations_1.o : theories/Sets/Relations_1.hs
+theories/Sets/Relations_1_facts.o : theories/Sets/Relations_1_facts.hs
+theories/Sets/Relations_2.o : theories/Sets/Relations_2.hs
+theories/Sets/Relations_2_facts.o : theories/Sets/Relations_2_facts.hs
+theories/Sets/Relations_3.o : theories/Sets/Relations_3.hs
+theories/Sets/Relations_3_facts.o : theories/Sets/Relations_3_facts.hs
+theories/Sets/Uniset.o : theories/Bool/Bool.o
+theories/Sets/Uniset.o : theories/Init/Datatypes.o
+theories/Sets/Uniset.o : theories/Init/Specif.o
+theories/Sets/Uniset.o : theories/Sets/Uniset.hs
+theories/Sorting/Heap.o : theories/Init/Logic.o
+theories/Sorting/Heap.o : theories/Init/Specif.o
+theories/Sorting/Heap.o : theories/Lists/PolyList.o
+theories/Sorting/Heap.o : theories/Sets/Multiset.o
+theories/Sorting/Heap.o : theories/Sorting/Heap.hs
+theories/Sorting/Heap.o : theories/Sorting/Sorting.o
+theories/Sorting/Permutation.o : theories/Lists/PolyList.o
+theories/Sorting/Permutation.o : theories/Sets/Multiset.o
+theories/Sorting/Permutation.o : theories/Sorting/Permutation.hs
+theories/Sorting/Sorting.o : theories/Init/Logic.o
+theories/Sorting/Sorting.o : theories/Init/Specif.o
+theories/Sorting/Sorting.o : theories/Lists/PolyList.o
+theories/Sorting/Sorting.o : theories/Sorting/Sorting.hs
+theories/Wellfounded/Disjoint_Union.o : theories/Wellfounded/Disjoint_Union.hs
+theories/Wellfounded/Inclusion.o : theories/Wellfounded/Inclusion.hs
+theories/Wellfounded/Inverse_Image.o : theories/Wellfounded/Inverse_Image.hs
+theories/Wellfounded/Lexicographic_Exponentiation.o : theories/Wellfounded/Lexicographic_Exponentiation.hs
+theories/Wellfounded/Lexicographic_Product.o : theories/Wellfounded/Lexicographic_Product.hs
+theories/Wellfounded/Transitive_Closure.o : theories/Wellfounded/Transitive_Closure.hs
+theories/Wellfounded/Union.o : theories/Wellfounded/Union.hs
+theories/Wellfounded/Well_Ordering.o : theories/Init/Specif.o
+theories/Wellfounded/Well_Ordering.o : theories/Init/Wf.o
+theories/Wellfounded/Well_Ordering.o : theories/Wellfounded/Well_Ordering.hs
+theories/Wellfounded/Wellfounded.o : theories/Wellfounded/Wellfounded.hs
+theories/ZArith/Auxiliary.o : theories/ZArith/Auxiliary.hs
+theories/ZArith/Fast_integer.o : theories/Init/Datatypes.o
+theories/ZArith/Fast_integer.o : theories/Init/Peano.o
+theories/ZArith/Fast_integer.o : theories/ZArith/Fast_integer.hs
+theories/ZArith/Wf_Z.o : theories/Init/Datatypes.o
+theories/ZArith/Wf_Z.o : theories/Init/Logic.o
+theories/ZArith/Wf_Z.o : theories/Init/Peano.o
+theories/ZArith/Wf_Z.o : theories/Init/Specif.o
+theories/ZArith/Wf_Z.o : theories/ZArith/Fast_integer.o
+theories/ZArith/Wf_Z.o : theories/ZArith/Wf_Z.hs
+theories/ZArith/Wf_Z.o : theories/ZArith/Zarith_aux.o
+theories/ZArith/ZArith.o : theories/ZArith/ZArith.hs
+theories/ZArith/ZArith_dec.o : theories/Bool/Sumbool.o
+theories/ZArith/ZArith_dec.o : theories/Init/Logic.o
+theories/ZArith/ZArith_dec.o : theories/Init/Specif.o
+theories/ZArith/ZArith_dec.o : theories/ZArith/Fast_integer.o
+theories/ZArith/ZArith_dec.o : theories/ZArith/ZArith_dec.hs
+theories/ZArith/Zarith_aux.o : theories/Init/Datatypes.o
+theories/ZArith/Zarith_aux.o : theories/Init/Specif.o
+theories/ZArith/Zarith_aux.o : theories/ZArith/Fast_integer.o
+theories/ZArith/Zarith_aux.o : theories/ZArith/Zarith_aux.hs
+theories/ZArith/Zcomplements.o : theories/Init/Datatypes.o
+theories/ZArith/Zcomplements.o : theories/Init/Logic.o
+theories/ZArith/Zcomplements.o : theories/Init/Specif.o
+theories/ZArith/Zcomplements.o : theories/ZArith/Fast_integer.o
+theories/ZArith/Zcomplements.o : theories/ZArith/Wf_Z.o
+theories/ZArith/Zcomplements.o : theories/ZArith/ZArith_dec.o
+theories/ZArith/Zcomplements.o : theories/ZArith/Zarith_aux.o
+theories/ZArith/Zcomplements.o : theories/ZArith/Zcomplements.hs
+theories/ZArith/Zhints.o : theories/ZArith/Zhints.hs
+theories/ZArith/Zlogarithm.o : theories/ZArith/Fast_integer.o
+theories/ZArith/Zlogarithm.o : theories/ZArith/Zarith_aux.o
+theories/ZArith/Zlogarithm.o : theories/ZArith/Zlogarithm.hs
+theories/ZArith/Zmisc.o : theories/Init/Datatypes.o
+theories/ZArith/Zmisc.o : theories/Init/Specif.o
+theories/ZArith/Zmisc.o : theories/ZArith/Fast_integer.o
+theories/ZArith/Zmisc.o : theories/ZArith/Zmisc.hs
+theories/ZArith/Zpower.o : theories/Init/Datatypes.o
+theories/ZArith/Zpower.o : theories/Init/Logic.o
+theories/ZArith/Zpower.o : theories/ZArith/Fast_integer.o
+theories/ZArith/Zpower.o : theories/ZArith/Zarith_aux.o
+theories/ZArith/Zpower.o : theories/ZArith/Zmisc.o
+theories/ZArith/Zpower.o : theories/ZArith/Zpower.hs
+# DO NOT DELETE: End of Haskell dependencies
diff --git a/contrib/extraction/test/Unit.hs b/contrib/extraction/test/Unit.hs
new file mode 100644
index 000000000..2001dfa1b
--- /dev/null
+++ b/contrib/extraction/test/Unit.hs
@@ -0,0 +1,5 @@
+module Unit where 
+
+type Unit = ()
+unit = ()
+
diff --git a/contrib/extraction/test/extract.haskell b/contrib/extraction/test/extract.haskell
new file mode 100755
index 000000000..ef98a62ed
--- /dev/null
+++ b/contrib/extraction/test/extract.haskell
@@ -0,0 +1,13 @@
+#!/bin/sh
+rm -f /tmp/extr$$.v 
+vfile=`./hs2v $1`
+d=`dirname $vfile`
+n=`basename $vfile .v`
+cat custom/all > /tmp/extr$$.v
+if [ -e custom/$n ]; then cat custom/$n >> /tmp/extr$$.v; fi  
+echo "Cd \"$d\". Haskell Extraction Module $n. " >> /tmp/extr$$.v
+../../../bin/coqtop.opt -silent -batch -require $n -load-vernac-source /tmp/extr$$.v 
+out=$?
+rm -f /tmp/extr$$.v
+exit $out
+
diff --git a/contrib/extraction/test/hs2v.ml b/contrib/extraction/test/hs2v.ml
new file mode 100644
index 000000000..fd8b9b269
--- /dev/null
+++ b/contrib/extraction/test/hs2v.ml
@@ -0,0 +1,14 @@
+let _ =
+  for j = 1 to ((Array.length Sys.argv)-1) do
+    let fml = Sys.argv.(j) in
+    let f = Filename.chop_extension fml in 
+    let fv = f ^ ".v" in
+    if Sys.file_exists ("../../../" ^ fv) then
+      print_string (fv^" ") 
+    else
+      let d = Filename.dirname f in
+      let b = String.uncapitalize (Filename.basename f) in
+      let fv = Filename.concat d (b ^ ".v ") in
+      print_string fv
+  done;
+  print_newline()
diff --git a/contrib/extraction/test/v2hs.ml b/contrib/extraction/test/v2hs.ml
new file mode 100644
index 000000000..886328754
--- /dev/null
+++ b/contrib/extraction/test/v2hs.ml
@@ -0,0 +1,9 @@
+let _ = 
+  for j = 1 to ((Array.length Sys.argv) -1) do 
+    let s = Sys.argv.(j) in
+    let b = Filename.chop_extension (Filename.basename s) in 
+    let b = String.capitalize b in
+    let d = Filename.dirname s in 
+    print_string (Filename.concat d (b ^ ".hs "))
+  done;	
+  print_newline()