Extraction des modules, enfin !

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

3 files changed, 264 insertions, 195 deletions

diff --git a/contrib/extraction/test/.depend b/contrib/extraction/test/.depend
index 952a8e087e..f70e81319a 100644
--- a/contrib/extraction/test/.depend
+++ b/contrib/extraction/test/.depend
@@ -78,6 +78,12 @@ theories/Bool/bool.cmo: theories/Init/datatypes.cmi theories/Init/specif.cmi \
     theories/Bool/bool.cmi 
 theories/Bool/bool.cmx: theories/Init/datatypes.cmx theories/Init/specif.cmx \
     theories/Bool/bool.cmi 
+theories/Bool/bvector.cmo: theories/Bool/bool.cmi theories/Init/datatypes.cmi \
+    theories/Arith/minus.cmi theories/Init/peano.cmi \
+    theories/Bool/bvector.cmi 
+theories/Bool/bvector.cmx: theories/Bool/bool.cmx theories/Init/datatypes.cmx \
+    theories/Arith/minus.cmx theories/Init/peano.cmx \
+    theories/Bool/bvector.cmi 
 theories/Bool/decBool.cmo: theories/Init/specif.cmi theories/Bool/decBool.cmi 
 theories/Bool/decBool.cmx: theories/Init/specif.cmx theories/Bool/decBool.cmi 
 theories/Bool/ifProp.cmo: theories/Init/datatypes.cmi \
@@ -156,16 +162,16 @@ theories/IntMap/fset.cmx: theories/IntMap/addec.cmx theories/IntMap/addr.cmx \
     theories/Init/specif.cmx theories/IntMap/fset.cmi 
 theories/IntMap/lsort.cmo: theories/IntMap/addec.cmi theories/IntMap/addr.cmi \
     theories/Bool/bool.cmi theories/Init/datatypes.cmi \
-    theories/ZArith/fast_integer.cmi theories/IntMap/map.cmi \
-    theories/IntMap/mapiter.cmi theories/Lists/polyList.cmi \
-    theories/Init/specif.cmi theories/Bool/sumbool.cmi \
-    theories/IntMap/lsort.cmi 
+    theories/ZArith/fast_integer.cmi theories/Init/logic.cmi \
+    theories/IntMap/map.cmi theories/IntMap/mapiter.cmi \
+    theories/Lists/polyList.cmi theories/Init/specif.cmi \
+    theories/Bool/sumbool.cmi theories/IntMap/lsort.cmi 
 theories/IntMap/lsort.cmx: theories/IntMap/addec.cmx theories/IntMap/addr.cmx \
     theories/Bool/bool.cmx theories/Init/datatypes.cmx \
-    theories/ZArith/fast_integer.cmx theories/IntMap/map.cmx \
-    theories/IntMap/mapiter.cmx theories/Lists/polyList.cmx \
-    theories/Init/specif.cmx theories/Bool/sumbool.cmx \
-    theories/IntMap/lsort.cmi 
+    theories/ZArith/fast_integer.cmx theories/Init/logic.cmx \
+    theories/IntMap/map.cmx theories/IntMap/mapiter.cmx \
+    theories/Lists/polyList.cmx theories/Init/specif.cmx \
+    theories/Bool/sumbool.cmx theories/IntMap/lsort.cmi 
 theories/IntMap/mapaxioms.cmo: theories/IntMap/mapaxioms.cmi 
 theories/IntMap/mapaxioms.cmx: theories/IntMap/mapaxioms.cmi 
 theories/IntMap/mapcanon.cmo: theories/IntMap/map.cmi \
@@ -174,13 +180,13 @@ theories/IntMap/mapcanon.cmx: theories/IntMap/map.cmx \
     theories/Init/specif.cmx theories/IntMap/mapcanon.cmi 
 theories/IntMap/mapcard.cmo: theories/IntMap/addec.cmi \
     theories/IntMap/addr.cmi theories/Init/datatypes.cmi \
-    theories/IntMap/map.cmi theories/Init/peano.cmi \
+    theories/Init/logic.cmi theories/IntMap/map.cmi theories/Init/peano.cmi \
     theories/Arith/peano_dec.cmi theories/Arith/plus.cmi \
     theories/Init/specif.cmi theories/Bool/sumbool.cmi \
     theories/IntMap/mapcard.cmi 
 theories/IntMap/mapcard.cmx: theories/IntMap/addec.cmx \
     theories/IntMap/addr.cmx theories/Init/datatypes.cmx \
-    theories/IntMap/map.cmx theories/Init/peano.cmx \
+    theories/Init/logic.cmx theories/IntMap/map.cmx theories/Init/peano.cmx \
     theories/Arith/peano_dec.cmx theories/Arith/plus.cmx \
     theories/Init/specif.cmx theories/Bool/sumbool.cmx \
     theories/IntMap/mapcard.cmi 
@@ -357,13 +363,15 @@ theories/Sets/uniset.cmo: theories/Init/datatypes.cmi \
 theories/Sets/uniset.cmx: theories/Init/datatypes.cmx \
     theories/Init/specif.cmx theories/Sets/uniset.cmi 
 theories/Sorting/heap.cmo: theories/Init/datatypes.cmi \
-    theories/Sets/multiset.cmi theories/Init/peano.cmi \
-    theories/Lists/polyList.cmi theories/Sorting/sorting.cmi \
-    theories/Init/specif.cmi theories/Sorting/heap.cmi 
+    theories/Init/logic.cmi theories/Sets/multiset.cmi \
+    theories/Init/peano.cmi theories/Lists/polyList.cmi \
+    theories/Sorting/sorting.cmi theories/Init/specif.cmi \
+    theories/Sorting/heap.cmi 
 theories/Sorting/heap.cmx: theories/Init/datatypes.cmx \
-    theories/Sets/multiset.cmx theories/Init/peano.cmx \
-    theories/Lists/polyList.cmx theories/Sorting/sorting.cmx \
-    theories/Init/specif.cmx theories/Sorting/heap.cmi 
+    theories/Init/logic.cmx theories/Sets/multiset.cmx \
+    theories/Init/peano.cmx theories/Lists/polyList.cmx \
+    theories/Sorting/sorting.cmx theories/Init/specif.cmx \
+    theories/Sorting/heap.cmi 
 theories/Sorting/permutation.cmo: theories/Init/datatypes.cmi \
     theories/Sets/multiset.cmi theories/Init/peano.cmi \
     theories/Lists/polyList.cmi theories/Init/specif.cmi \
@@ -372,10 +380,12 @@ theories/Sorting/permutation.cmx: theories/Init/datatypes.cmx \
     theories/Sets/multiset.cmx theories/Init/peano.cmx \
     theories/Lists/polyList.cmx theories/Init/specif.cmx \
     theories/Sorting/permutation.cmi 
-theories/Sorting/sorting.cmo: theories/Lists/polyList.cmi \
-    theories/Init/specif.cmi theories/Sorting/sorting.cmi 
-theories/Sorting/sorting.cmx: theories/Lists/polyList.cmx \
-    theories/Init/specif.cmx theories/Sorting/sorting.cmi 
+theories/Sorting/sorting.cmo: theories/Init/logic.cmi \
+    theories/Lists/polyList.cmi theories/Init/specif.cmi \
+    theories/Sorting/sorting.cmi 
+theories/Sorting/sorting.cmx: theories/Init/logic.cmx \
+    theories/Lists/polyList.cmx theories/Init/specif.cmx \
+    theories/Sorting/sorting.cmi 
 theories/Wellfounded/disjoint_Union.cmo: \
     theories/Wellfounded/disjoint_Union.cmi 
 theories/Wellfounded/disjoint_Union.cmx: \
@@ -436,6 +446,14 @@ theories/ZArith/zArith_dec.cmx: theories/ZArith/fast_integer.cmx \
     theories/ZArith/zArith_dec.cmi 
 theories/ZArith/zArith.cmo: theories/ZArith/zArith.cmi 
 theories/ZArith/zArith.cmx: theories/ZArith/zArith.cmi 
+theories/ZArith/zbinary.cmo: theories/Bool/bvector.cmi \
+    theories/Init/datatypes.cmi theories/ZArith/fast_integer.cmi \
+    theories/ZArith/zarith_aux.cmi theories/ZArith/zmisc.cmi \
+    theories/ZArith/zbinary.cmi 
+theories/ZArith/zbinary.cmx: theories/Bool/bvector.cmx \
+    theories/Init/datatypes.cmx theories/ZArith/fast_integer.cmx \
+    theories/ZArith/zarith_aux.cmx theories/ZArith/zmisc.cmx \
+    theories/ZArith/zbinary.cmi 
 theories/ZArith/zbool.cmo: theories/Init/datatypes.cmi \
     theories/ZArith/fast_integer.cmi theories/Init/specif.cmi \
     theories/Bool/sumbool.cmi theories/ZArith/zArith_dec.cmi \
@@ -473,11 +491,13 @@ theories/ZArith/zmisc.cmx: theories/Init/datatypes.cmx \
     theories/ZArith/fast_integer.cmx theories/Init/specif.cmx \
     theories/ZArith/zmisc.cmi 
 theories/ZArith/zpower.cmo: theories/Init/datatypes.cmi \
-    theories/ZArith/fast_integer.cmi theories/ZArith/zarith_aux.cmi \
-    theories/ZArith/zmisc.cmi theories/ZArith/zpower.cmi 
+    theories/ZArith/fast_integer.cmi theories/Init/logic.cmi \
+    theories/ZArith/zarith_aux.cmi theories/ZArith/zmisc.cmi \
+    theories/ZArith/zpower.cmi 
 theories/ZArith/zpower.cmx: theories/Init/datatypes.cmx \
-    theories/ZArith/fast_integer.cmx theories/ZArith/zarith_aux.cmx \
-    theories/ZArith/zmisc.cmx theories/ZArith/zpower.cmi 
+    theories/ZArith/fast_integer.cmx theories/Init/logic.cmx \
+    theories/ZArith/zarith_aux.cmx theories/ZArith/zmisc.cmx \
+    theories/ZArith/zpower.cmi 
 theories/ZArith/zsqrt.cmo: theories/ZArith/fast_integer.cmi \
     theories/Init/specif.cmi theories/ZArith/zArith_dec.cmi \
     theories/ZArith/zarith_aux.cmi theories/ZArith/zsqrt.cmi 
@@ -512,6 +532,8 @@ theories/Arith/wf_nat.cmi: theories/Init/datatypes.cmi
 theories/Bool/boolEq.cmi: theories/Init/datatypes.cmi \
     theories/Init/specif.cmi 
 theories/Bool/bool.cmi: theories/Init/datatypes.cmi theories/Init/specif.cmi 
+theories/Bool/bvector.cmi: theories/Bool/bool.cmi theories/Init/datatypes.cmi \
+    theories/Arith/minus.cmi theories/Init/peano.cmi 
 theories/Bool/decBool.cmi: theories/Init/specif.cmi 
 theories/Bool/ifProp.cmi: theories/Init/datatypes.cmi \
     theories/Init/specif.cmi 
@@ -537,14 +559,15 @@ theories/IntMap/fset.cmi: theories/IntMap/addec.cmi theories/IntMap/addr.cmi \
     theories/Init/specif.cmi 
 theories/IntMap/lsort.cmi: theories/IntMap/addec.cmi theories/IntMap/addr.cmi \
     theories/Bool/bool.cmi theories/Init/datatypes.cmi \
-    theories/ZArith/fast_integer.cmi theories/IntMap/map.cmi \
-    theories/IntMap/mapiter.cmi theories/Lists/polyList.cmi \
-    theories/Init/specif.cmi theories/Bool/sumbool.cmi 
+    theories/ZArith/fast_integer.cmi theories/Init/logic.cmi \
+    theories/IntMap/map.cmi theories/IntMap/mapiter.cmi \
+    theories/Lists/polyList.cmi theories/Init/specif.cmi \
+    theories/Bool/sumbool.cmi 
 theories/IntMap/mapcanon.cmi: theories/IntMap/map.cmi \
     theories/Init/specif.cmi 
 theories/IntMap/mapcard.cmi: theories/IntMap/addec.cmi \
     theories/IntMap/addr.cmi theories/Init/datatypes.cmi \
-    theories/IntMap/map.cmi theories/Init/peano.cmi \
+    theories/Init/logic.cmi theories/IntMap/map.cmi theories/Init/peano.cmi \
     theories/Arith/peano_dec.cmi theories/Arith/plus.cmi \
     theories/Init/specif.cmi theories/Bool/sumbool.cmi 
 theories/IntMap/mapfold.cmi: theories/IntMap/addr.cmi \
@@ -584,14 +607,14 @@ theories/Sets/powerset.cmi: theories/Sets/partial_Order.cmi
 theories/Sets/uniset.cmi: theories/Init/datatypes.cmi \
     theories/Init/specif.cmi 
 theories/Sorting/heap.cmi: theories/Init/datatypes.cmi \
-    theories/Sets/multiset.cmi theories/Init/peano.cmi \
-    theories/Lists/polyList.cmi theories/Sorting/sorting.cmi \
-    theories/Init/specif.cmi 
+    theories/Init/logic.cmi theories/Sets/multiset.cmi \
+    theories/Init/peano.cmi theories/Lists/polyList.cmi \
+    theories/Sorting/sorting.cmi theories/Init/specif.cmi 
 theories/Sorting/permutation.cmi: theories/Init/datatypes.cmi \
     theories/Sets/multiset.cmi theories/Init/peano.cmi \
     theories/Lists/polyList.cmi theories/Init/specif.cmi 
-theories/Sorting/sorting.cmi: theories/Lists/polyList.cmi \
-    theories/Init/specif.cmi 
+theories/Sorting/sorting.cmi: theories/Init/logic.cmi \
+    theories/Lists/polyList.cmi theories/Init/specif.cmi 
 theories/Wellfounded/well_Ordering.cmi: theories/Init/specif.cmi 
 theories/ZArith/fast_integer.cmi: theories/Init/datatypes.cmi \
     theories/Init/peano.cmi 
@@ -602,6 +625,9 @@ theories/ZArith/zarith_aux.cmi: theories/Init/datatypes.cmi \
     theories/ZArith/fast_integer.cmi theories/Init/specif.cmi 
 theories/ZArith/zArith_dec.cmi: theories/ZArith/fast_integer.cmi \
     theories/Init/specif.cmi theories/Bool/sumbool.cmi 
+theories/ZArith/zbinary.cmi: theories/Bool/bvector.cmi \
+    theories/Init/datatypes.cmi theories/ZArith/fast_integer.cmi \
+    theories/ZArith/zarith_aux.cmi theories/ZArith/zmisc.cmi 
 theories/ZArith/zbool.cmi: theories/Init/datatypes.cmi \
     theories/ZArith/fast_integer.cmi theories/Init/specif.cmi \
     theories/Bool/sumbool.cmi theories/ZArith/zArith_dec.cmi \
@@ -618,8 +644,8 @@ theories/ZArith/zlogarithm.cmi: theories/ZArith/fast_integer.cmi \
 theories/ZArith/zmisc.cmi: theories/Init/datatypes.cmi \
     theories/ZArith/fast_integer.cmi theories/Init/specif.cmi 
 theories/ZArith/zpower.cmi: theories/Init/datatypes.cmi \
-    theories/ZArith/fast_integer.cmi theories/ZArith/zarith_aux.cmi \
-    theories/ZArith/zmisc.cmi 
+    theories/ZArith/fast_integer.cmi theories/Init/logic.cmi \
+    theories/ZArith/zarith_aux.cmi theories/ZArith/zmisc.cmi 
 theories/ZArith/zsqrt.cmi: theories/ZArith/fast_integer.cmi \
     theories/Init/specif.cmi theories/ZArith/zArith_dec.cmi \
     theories/ZArith/zarith_aux.cmi 
diff --git a/contrib/extraction/test/Makefile b/contrib/extraction/test/Makefile
index 646e8b6ba0..4ab5fe7fb7 100644
--- a/contrib/extraction/test/Makefile
+++ b/contrib/extraction/test/Makefile
@@ -42,8 +42,8 @@ depend: $(ML)
 tree:
 	mkdir -p $(DIRS)
 
-%.mli:%.ml
-	./make_mli $< > $@
+#%.mli:%.ml
+#	./make_mli $< > $@
 
 %.cmi:%.mli
 	ocamlc $(INCL) -c -i $<
diff --git a/contrib/extraction/test/Makefile.haskell b/contrib/extraction/test/Makefile.haskell
index 347e998874..bd50f9bf51 100644
--- a/contrib/extraction/test/Makefile.haskell
+++ b/contrib/extraction/test/Makefile.haskell
@@ -7,6 +7,7 @@ TOPDIR=../../..
 # Files with axioms to be realized: can't be extracted directly
 
 AXIOMSVO:= \
+theories/Init/PeanoSyntax.vo \
 theories/Init/Prelude.vo \
 theories/Arith/Arith.vo \
 theories/Lists/List.vo \
@@ -68,69 +69,77 @@ v2hs: v2hs.ml
 
 # 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/Bool_nat.o : theories/Arith/Bool_nat.hs
+theories/Arith/Bool_nat.o : theories/Bool/Sumbool.o
+theories/Arith/Bool_nat.o : theories/Init/Specif.o
+theories/Arith/Bool_nat.o : theories/Arith/Peano_dec.o
+theories/Arith/Bool_nat.o : theories/Init/Datatypes.o
+theories/Arith/Bool_nat.o : theories/Arith/Compare_dec.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/Compare_dec.o : theories/Init/Logic.o
+theories/Arith/Compare_dec.o : theories/Init/Datatypes.o
+theories/Arith/Compare.o : theories/Arith/Compare.hs
+theories/Arith/Compare.o : theories/Init/Specif.o
+theories/Arith/Compare.o : theories/Init/Datatypes.o
+theories/Arith/Compare.o : theories/Arith/Compare_dec.o
 theories/Arith/Div2.o : theories/Arith/Div2.hs
-theories/Arith/Div2.o : theories/Init/Datatypes.o
+theories/Arith/Div2.o : theories/Init/Specif.o
 theories/Arith/Div2.o : theories/Init/Peano.o
+theories/Arith/Div2.o : theories/Init/Datatypes.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/EqNat.o : theories/Init/Datatypes.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/Euclid.o : theories/Arith/Minus.o
+theories/Arith/Euclid.o : theories/Init/Datatypes.o
+theories/Arith/Euclid.o : theories/Arith/Compare_dec.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/Even.o : theories/Init/Datatypes.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/Max.o : theories/Init/Logic.o
+theories/Arith/Max.o : theories/Init/Datatypes.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/Min.o : theories/Init/Logic.o
+theories/Arith/Min.o : theories/Init/Datatypes.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/Peano_dec.o : theories/Init/Datatypes.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/Plus.o : theories/Init/Logic.o
+theories/Arith/Plus.o : theories/Init/Datatypes.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/Arith/Wf_nat.o : theories/Init/Logic.o
+theories/Arith/Wf_nat.o : theories/Init/Datatypes.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/BoolEq.o : theories/Init/Datatypes.o
+theories/Bool/Bool.o : theories/Bool/Bool.hs
+theories/Bool/Bool.o : theories/Init/Specif.o
+theories/Bool/Bool.o : theories/Init/Datatypes.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/IfProp.o : theories/Init/Datatypes.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/Sumbool.o : theories/Init/Datatypes.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
@@ -139,188 +148,200 @@ 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/Peano.o : theories/Init/Datatypes.o
 theories/Init/Specif.o : theories/Init/Specif.hs
+theories/Init/Specif.o : theories/Init/Logic.o
+theories/Init/Specif.o : theories/Init/Datatypes.o
 theories/Init/SpecifSyntax.o : theories/Init/SpecifSyntax.hs
 theories/Init/Wf.o : theories/Init/Wf.hs
+theories/IntMap/Adalloc.o : theories/IntMap/Adalloc.hs
+theories/IntMap/Adalloc.o : theories/ZArith/Fast_integer.o
 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/Adalloc.o : theories/Init/Logic.o
+theories/IntMap/Adalloc.o : theories/Init/Datatypes.o
+theories/IntMap/Adalloc.o : theories/IntMap/Addr.o
+theories/IntMap/Adalloc.o : theories/IntMap/Addec.o
+theories/IntMap/Addec.o : theories/IntMap/Addec.hs
+theories/IntMap/Addec.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/Init/Datatypes.o
 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/Addr.o : theories/Init/Specif.o
+theories/IntMap/Addr.o : theories/Init/Datatypes.o
+theories/IntMap/Addr.o : theories/Bool/Bool.o
+theories/IntMap/Adist.o : theories/IntMap/Adist.hs
+theories/IntMap/Adist.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/Init/Specif.o
 theories/IntMap/Fset.o : theories/IntMap/Map.o
-theories/IntMap/Lsort.o : theories/Bool/Bool.o
+theories/IntMap/Fset.o : theories/Init/Logic.o
+theories/IntMap/Fset.o : theories/Init/Datatypes.o
+theories/IntMap/Fset.o : theories/IntMap/Addr.o
+theories/IntMap/Fset.o : theories/IntMap/Addec.o
+theories/IntMap/Lsort.o : theories/IntMap/Lsort.hs
+theories/IntMap/Lsort.o : theories/ZArith/Fast_integer.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/Lsort.o : theories/IntMap/Mapiter.o
+theories/IntMap/Lsort.o : theories/IntMap/Map.o
+theories/IntMap/Lsort.o : theories/Init/Logic.o
+theories/IntMap/Lsort.o : theories/Init/Datatypes.o
+theories/IntMap/Lsort.o : theories/Bool/Bool.o
+theories/IntMap/Lsort.o : theories/IntMap/Addr.o
+theories/IntMap/Lsort.o : theories/IntMap/Addec.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/Mapcanon.o : theories/Init/Specif.o
+theories/IntMap/Mapcanon.o : theories/IntMap/Map.o
+theories/IntMap/Mapcard.o : theories/IntMap/Mapcard.hs
 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/Arith/Plus.o
+theories/IntMap/Mapcard.o : theories/Arith/Peano_dec.o
+theories/IntMap/Mapcard.o : theories/Init/Peano.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/Mapcard.o : theories/Init/Logic.o
+theories/IntMap/Mapcard.o : theories/Init/Datatypes.o
+theories/IntMap/Mapcard.o : theories/IntMap/Addr.o
+theories/IntMap/Mapcard.o : theories/IntMap/Addec.o
+theories/IntMap/Mapc.o : theories/IntMap/Mapc.hs
 theories/IntMap/Mapfold.o : theories/IntMap/Mapfold.hs
+theories/IntMap/Mapfold.o : theories/Init/Specif.o
 theories/IntMap/Mapfold.o : theories/IntMap/Mapiter.o
+theories/IntMap/Mapfold.o : theories/IntMap/Map.o
+theories/IntMap/Mapfold.o : theories/Init/Logic.o
+theories/IntMap/Mapfold.o : theories/IntMap/Fset.o
+theories/IntMap/Mapfold.o : theories/Init/Datatypes.o
+theories/IntMap/Mapfold.o : theories/IntMap/Addr.o
+theories/IntMap/Map.o : theories/IntMap/Map.hs
+theories/IntMap/Map.o : theories/ZArith/Fast_integer.o
+theories/IntMap/Map.o : theories/Init/Specif.o
+theories/IntMap/Map.o : theories/Init/Peano.o
+theories/IntMap/Map.o : theories/Init/Datatypes.o
+theories/IntMap/Map.o : theories/IntMap/Addr.o
+theories/IntMap/Map.o : theories/IntMap/Addec.o
+theories/IntMap/Mapiter.o : theories/IntMap/Mapiter.hs
 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/Mapiter.o : theories/IntMap/Map.o
+theories/IntMap/Mapiter.o : theories/Init/Logic.o
+theories/IntMap/Mapiter.o : theories/Init/Datatypes.o
+theories/IntMap/Mapiter.o : theories/IntMap/Addr.o
+theories/IntMap/Mapiter.o : theories/IntMap/Addec.o
+theories/IntMap/Maplists.o : theories/IntMap/Maplists.hs
 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/Maplists.o : theories/IntMap/Mapiter.o
+theories/IntMap/Maplists.o : theories/IntMap/Map.o
+theories/IntMap/Maplists.o : theories/Init/Logic.o
+theories/IntMap/Maplists.o : theories/IntMap/Fset.o
+theories/IntMap/Maplists.o : theories/Init/Datatypes.o
+theories/IntMap/Maplists.o : theories/Bool/Bool.o
+theories/IntMap/Maplists.o : theories/IntMap/Addr.o
+theories/IntMap/Maplists.o : theories/IntMap/Addec.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/IntMap/Mapsubset.o : theories/IntMap/Mapiter.o
+theories/IntMap/Mapsubset.o : theories/IntMap/Map.o
+theories/IntMap/Mapsubset.o : theories/IntMap/Fset.o
+theories/IntMap/Mapsubset.o : theories/Init/Datatypes.o
+theories/IntMap/Mapsubset.o : theories/Bool/Bool.o
 theories/Lists/ListSet.o : theories/Lists/ListSet.hs
+theories/Lists/ListSet.o : theories/Init/Specif.o
 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/ListSet.o : theories/Init/Logic.o
+theories/Lists/ListSet.o : theories/Init/Datatypes.o
 theories/Lists/PolyList.o : theories/Lists/PolyList.hs
+theories/Lists/PolyList.o : theories/Init/Specif.o
+theories/Lists/PolyList.o : theories/Init/Datatypes.o
 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/Streams.o : theories/Init/Datatypes.o
+theories/Lists/TheoryList.o : theories/Lists/TheoryList.hs
 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/Lists/TheoryList.o : theories/Bool/DecBool.o
+theories/Lists/TheoryList.o : theories/Init/Datatypes.o
 theories/Logic/Berardi.o : theories/Logic/Berardi.hs
+theories/Logic/ClassicalFacts.o : theories/Logic/ClassicalFacts.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/Eqdep.o : theories/Logic/Eqdep.hs
+theories/Logic/Hurkens.o : theories/Logic/Hurkens.hs
 theories/Logic/JMeq.o : theories/Logic/JMeq.hs
+theories/Logic/ProofIrrelevance.o : theories/Logic/ProofIrrelevance.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/Relation_Operators.o : theories/Init/Specif.o
+theories/Relations/Relation_Operators.o : theories/Lists/PolyList.o
 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/Cpo.o : theories/Sets/Partial_Order.o
 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/Finite_sets.o : theories/Sets/Finite_sets.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/Integers.o : theories/Init/Datatypes.o
 theories/Sets/Multiset.o : theories/Sets/Multiset.hs
+theories/Sets/Multiset.o : theories/Init/Specif.o
+theories/Sets/Multiset.o : theories/Init/Peano.o
+theories/Sets/Multiset.o : theories/Init/Datatypes.o
 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/Powerset.o : theories/Sets/Powerset.hs
+theories/Sets/Powerset.o : theories/Sets/Partial_Order.o
 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_1.o : theories/Sets/Relations_1.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_2.o : theories/Sets/Relations_2.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/Relations_3.o : theories/Sets/Relations_3.hs
 theories/Sets/Uniset.o : theories/Sets/Uniset.hs
-theories/Sorting/Heap.o : theories/Init/Logic.o
+theories/Sets/Uniset.o : theories/Init/Specif.o
+theories/Sets/Uniset.o : theories/Init/Datatypes.o
+theories/Sets/Uniset.o : theories/Bool/Bool.o
+theories/Sorting/Heap.o : theories/Sorting/Heap.hs
 theories/Sorting/Heap.o : theories/Init/Specif.o
+theories/Sorting/Heap.o : theories/Sorting/Sorting.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/Heap.o : theories/Init/Logic.o
+theories/Sorting/Permutation.o : theories/Sorting/Permutation.hs
+theories/Sorting/Permutation.o : theories/Init/Specif.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/Sorting/Sorting.hs
 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/Sorting/Sorting.o : theories/Init/Logic.o
 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
@@ -328,51 +349,73 @@ theories/Wellfounded/Lexicographic_Exponentiation.o : theories/Wellfounded/Lexic
 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/Wellfounded/Well_Ordering.o : theories/Wellfounded/Well_Ordering.hs
+theories/Wellfounded/Well_Ordering.o : theories/Init/Wf.o
+theories/Wellfounded/Well_Ordering.o : theories/Init/Specif.o
 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/Fast_integer.o : theories/Init/Peano.o
+theories/ZArith/Fast_integer.o : theories/Init/Datatypes.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/Wf_Z.o : theories/ZArith/Fast_integer.o
+theories/ZArith/Wf_Z.o : theories/Init/Specif.o
+theories/ZArith/Wf_Z.o : theories/Init/Peano.o
+theories/ZArith/Wf_Z.o : theories/Init/Logic.o
+theories/ZArith/Wf_Z.o : theories/Init/Datatypes.o
+theories/ZArith/Zarith_aux.o : theories/ZArith/Zarith_aux.hs
+theories/ZArith/Zarith_aux.o : theories/ZArith/Fast_integer.o
+theories/ZArith/Zarith_aux.o : theories/Init/Specif.o
+theories/ZArith/Zarith_aux.o : theories/Init/Datatypes.o
+theories/ZArith/ZArith_base.o : theories/ZArith/ZArith_base.hs
+theories/ZArith/ZArith_dec.o : theories/ZArith/ZArith_dec.hs
+theories/ZArith/ZArith_dec.o : theories/ZArith/Fast_integer.o
 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/ZArith_dec.o : theories/Init/Logic.o
+theories/ZArith/ZArith.o : theories/ZArith/ZArith.hs
+theories/ZArith/Zbool.o : theories/ZArith/Zbool.hs
+theories/ZArith/Zbool.o : theories/ZArith/Fast_integer.o
+theories/ZArith/Zbool.o : theories/ZArith/Zmisc.o
+theories/ZArith/Zbool.o : theories/ZArith/ZArith_dec.o
+theories/ZArith/Zbool.o : theories/Bool/Sumbool.o
+theories/ZArith/Zbool.o : theories/Init/Specif.o
+theories/ZArith/Zbool.o : theories/Init/Datatypes.o
+theories/ZArith/Zcomplements.o : theories/ZArith/Zcomplements.hs
+theories/ZArith/Zcomplements.o : theories/ZArith/Zarith_aux.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/Zcomplements.o : theories/Init/Specif.o
+theories/ZArith/Zcomplements.o : theories/Init/Logic.o
+theories/ZArith/Zcomplements.o : theories/Init/Datatypes.o
+theories/ZArith/Zdiv.o : theories/ZArith/Zdiv.hs
+theories/ZArith/Zdiv.o : theories/ZArith/Zarith_aux.o
+theories/ZArith/Zdiv.o : theories/ZArith/Fast_integer.o
+theories/ZArith/Zdiv.o : theories/ZArith/Zmisc.o
+theories/ZArith/Zdiv.o : theories/ZArith/ZArith_dec.o
+theories/ZArith/Zdiv.o : theories/Init/Specif.o
+theories/ZArith/Zdiv.o : theories/Init/Logic.o
+theories/ZArith/Zdiv.o : theories/Init/Datatypes.o
 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/Zlogarithm.o : theories/ZArith/Zarith_aux.o
+theories/ZArith/Zlogarithm.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/Zmisc.o : theories/ZArith/Fast_integer.o
+theories/ZArith/Zmisc.o : theories/Init/Specif.o
+theories/ZArith/Zmisc.o : theories/Init/Datatypes.o
+theories/ZArith/Zpower.o : theories/ZArith/Zpower.hs
 theories/ZArith/Zpower.o : theories/ZArith/Zarith_aux.o
+theories/ZArith/Zpower.o : theories/ZArith/Fast_integer.o
 theories/ZArith/Zpower.o : theories/ZArith/Zmisc.o
-theories/ZArith/Zpower.o : theories/ZArith/Zpower.hs
+theories/ZArith/Zpower.o : theories/Init/Logic.o
+theories/ZArith/Zpower.o : theories/Init/Datatypes.o
+theories/ZArith/Zsqrt.o : theories/ZArith/Zsqrt.hs
+theories/ZArith/Zsqrt.o : theories/ZArith/Zarith_aux.o
+theories/ZArith/Zsqrt.o : theories/ZArith/Fast_integer.o
+theories/ZArith/Zsqrt.o : theories/ZArith/ZArith_dec.o
+theories/ZArith/Zsqrt.o : theories/Init/Specif.o
+theories/ZArith/Zsqrt.o : theories/Init/Logic.o
+theories/ZArith/Zwf.o : theories/ZArith/Zwf.hs
 # DO NOT DELETE: End of Haskell dependencies