Deplacement des fichiers ancienne syntaxe dans theories7, contrib7 et states7; Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states par les fichiers nouvelle syntaxe

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

4 files changed, 382 insertions, 106 deletions

diff --git a/.depend.coq b/.depend.coq
index 6d8bb59e2..93ef16e45 100644
--- a/.depend.coq
+++ b/.depend.coq
@@ -118,37 +118,32 @@ theories/NArith/Pnat.vo: theories/NArith/Pnat.v theories/NArith/BinPos.vo theori
 theories/NArith/BinNat.vo: theories/NArith/BinNat.v theories/NArith/BinPos.vo
 theories/NArith/NArith.vo: theories/NArith/NArith.v theories/NArith/BinPos.vo theories/NArith/BinNat.vo
 theories/ZArith/BinInt.vo: theories/ZArith/BinInt.v theories/NArith/BinPos.vo theories/NArith/Pnat.vo theories/NArith/BinNat.vo theories/Arith/Plus.vo theories/Arith/Mult.vo
-theories/ZArith/Wf_Z.vo: theories/ZArith/Wf_Z.v theories/ZArith/BinInt.vo theories/ZArith/Zcompare.vo theories/ZArith/Zorder.vo theories/ZArith/Znat.vo theories/ZArith/Zmisc.vo theories/ZArith/Zsyntax.vo theories/Arith/Wf_nat.vo
-theories/ZArith/Zsyntax.vo: theories/ZArith/Zsyntax.v theories/ZArith/BinInt.vo
+theories/ZArith/Wf_Z.vo: theories/ZArith/Wf_Z.v theories/ZArith/BinInt.vo theories/ZArith/Zcompare.vo theories/ZArith/Zorder.vo theories/ZArith/Znat.vo theories/ZArith/Zmisc.vo theories/Arith/Wf_nat.vo
 theories/ZArith/ZArith.vo: theories/ZArith/ZArith.v theories/ZArith/ZArith_base.vo theories/ZArith/Zcomplements.vo theories/ZArith/Zsqrt.vo theories/ZArith/Zpower.vo theories/ZArith/Zdiv.vo theories/ZArith/Zlogarithm.vo theories/ZArith/Zbool.vo
-theories/ZArith/auxiliary.vo: theories/ZArith/auxiliary.v theories/Arith/Arith.vo theories/ZArith/BinInt.vo theories/ZArith/Zorder.vo theories/Logic/Decidable.vo theories/Arith/Peano_dec.vo theories/Arith/Compare_dec.vo theories/ZArith/Znat.vo theories/ZArith/Zcompare.vo
-theories/ZArith/ZArith_dec.vo: theories/ZArith/ZArith_dec.v theories/Bool/Sumbool.vo theories/ZArith/BinInt.vo theories/ZArith/Zorder.vo theories/ZArith/Zcompare.vo theories/ZArith/Zsyntax.vo
-theories/ZArith/fast_integer.vo: theories/ZArith/fast_integer.v theories/NArith/BinPos.vo theories/NArith/BinNat.vo theories/ZArith/BinInt.vo theories/ZArith/Zcompare.vo theories/Arith/Mult.vo
-theories/ZArith/Zcompare.vo: theories/ZArith/Zcompare.v theories/NArith/BinPos.vo theories/ZArith/BinInt.vo theories/ZArith/Zsyntax.vo theories/Arith/Lt.vo theories/Arith/Gt.vo theories/Arith/Plus.vo theories/Arith/Mult.vo
+theories/ZArith/ZArith_dec.vo: theories/ZArith/ZArith_dec.v theories/Bool/Sumbool.vo theories/ZArith/BinInt.vo theories/ZArith/Zorder.vo theories/ZArith/Zcompare.vo
+theories/ZArith/auxiliary.vo: theories/ZArith/auxiliary.v theories/Arith/Arith.vo theories/ZArith/BinInt.vo theories/ZArith/Zorder.vo theories/Logic/Decidable.vo theories/Arith/Peano_dec.vo theories/Arith/Compare_dec.vo
+theories/ZArith/Zmisc.vo: theories/ZArith/Zmisc.v theories/ZArith/BinInt.vo theories/ZArith/Zcompare.vo theories/ZArith/Zorder.vo theories/Bool/Bool.vo
+theories/ZArith/Zcompare.vo: theories/ZArith/Zcompare.v theories/NArith/BinPos.vo theories/ZArith/BinInt.vo theories/Arith/Lt.vo theories/Arith/Gt.vo theories/Arith/Plus.vo theories/Arith/Mult.vo
 theories/ZArith/Znat.vo: theories/ZArith/Znat.v theories/Arith/Arith.vo theories/NArith/BinPos.vo theories/ZArith/BinInt.vo theories/ZArith/Zcompare.vo theories/ZArith/Zorder.vo theories/Logic/Decidable.vo theories/Arith/Peano_dec.vo theories/Arith/Compare_dec.vo
-theories/ZArith/Zmisc.vo: theories/ZArith/Zmisc.v theories/ZArith/BinInt.vo theories/ZArith/Zcompare.vo theories/ZArith/Zorder.vo theories/ZArith/Zsyntax.vo theories/Bool/Bool.vo theories/ZArith/Zbool.vo theories/ZArith/Zeven.vo theories/ZArith/Zabs.vo theories/ZArith/Zmin.vo
-theories/ZArith/zarith_aux.vo: theories/ZArith/zarith_aux.v theories/ZArith/BinInt.vo theories/ZArith/Zcompare.vo theories/ZArith/Zorder.vo theories/ZArith/Zmin.vo theories/ZArith/Zabs.vo
-theories/ZArith/Zorder.vo: theories/ZArith/Zorder.v theories/NArith/BinPos.vo theories/ZArith/BinInt.vo theories/Arith/Arith.vo theories/Logic/Decidable.vo theories/ZArith/Zsyntax.vo theories/ZArith/Zcompare.vo
-theories/ZArith/Zabs.vo: theories/ZArith/Zabs.v theories/Arith/Arith.vo theories/NArith/BinPos.vo theories/ZArith/BinInt.vo theories/ZArith/Zorder.vo theories/ZArith/Zsyntax.vo theories/ZArith/ZArith_dec.vo
+theories/ZArith/Zorder.vo: theories/ZArith/Zorder.v theories/NArith/BinPos.vo theories/ZArith/BinInt.vo theories/Arith/Arith.vo theories/Logic/Decidable.vo theories/ZArith/Zcompare.vo
+theories/ZArith/Zabs.vo: theories/ZArith/Zabs.v theories/Arith/Arith.vo theories/NArith/BinPos.vo theories/ZArith/BinInt.vo theories/ZArith/Zorder.vo theories/ZArith/ZArith_dec.vo
 theories/ZArith/Zmin.vo: theories/ZArith/Zmin.v theories/Arith/Arith.vo theories/ZArith/BinInt.vo theories/ZArith/Zcompare.vo theories/ZArith/Zorder.vo
-theories/ZArith/Zeven.vo: theories/ZArith/Zeven.v theories/ZArith/BinInt.vo theories/ZArith/Zsyntax.vo
-theories/ZArith/Zhints.vo: theories/ZArith/Zhints.v theories/ZArith/BinInt.vo theories/ZArith/Zorder.vo theories/ZArith/Zmin.vo theories/ZArith/Zabs.vo theories/ZArith/Zcompare.vo theories/ZArith/Znat.vo theories/ZArith/auxiliary.vo theories/ZArith/Zsyntax.vo theories/ZArith/Zmisc.vo theories/ZArith/Wf_Z.vo
+theories/ZArith/Zeven.vo: theories/ZArith/Zeven.v theories/ZArith/BinInt.vo
+theories/ZArith/Zhints.vo: theories/ZArith/Zhints.v theories/ZArith/BinInt.vo theories/ZArith/Zorder.vo theories/ZArith/Zmin.vo theories/ZArith/Zabs.vo theories/ZArith/Zcompare.vo theories/ZArith/Znat.vo theories/ZArith/auxiliary.vo theories/ZArith/Zmisc.vo theories/ZArith/Wf_Z.vo
 theories/ZArith/Zlogarithm.vo: theories/ZArith/Zlogarithm.v theories/ZArith/ZArith_base.vo contrib/omega/Omega.vo theories/ZArith/Zcomplements.vo theories/ZArith/Zpower.vo
 theories/ZArith/Zpower.vo: theories/ZArith/Zpower.v theories/ZArith/ZArith_base.vo contrib/omega/Omega.vo theories/ZArith/Zcomplements.vo
-theories/ZArith/Zcomplements.vo: theories/ZArith/Zcomplements.v contrib/ring/ZArithRing.vo theories/ZArith/ZArith_base.vo contrib/omega/Omega.vo theories/Arith/Wf_nat.vo theories/Lists/PolyList.vo
+theories/ZArith/Zcomplements.vo: theories/ZArith/Zcomplements.v contrib/ring/ZArithRing.vo theories/ZArith/ZArith_base.vo contrib/omega/Omega.vo theories/Arith/Wf_nat.vo theories/Lists/List.vo
 theories/ZArith/Zdiv.vo: theories/ZArith/Zdiv.v theories/ZArith/ZArith_base.vo theories/ZArith/Zbool.vo contrib/omega/Omega.vo contrib/ring/ZArithRing.vo theories/ZArith/Zcomplements.vo
 theories/ZArith/Zsqrt.vo: theories/ZArith/Zsqrt.v contrib/omega/Omega.vo theories/ZArith/ZArith_base.vo contrib/ring/ZArithRing.vo
 theories/ZArith/Zwf.vo: theories/ZArith/Zwf.v theories/ZArith/ZArith_base.vo theories/Arith/Wf_nat.vo contrib/omega/Omega.vo
-theories/ZArith/ZArith_base.vo: theories/ZArith/ZArith_base.v theories/ZArith/fast_integer.vo theories/ZArith/zarith_aux.vo theories/NArith/BinPos.vo theories/NArith/BinNat.vo theories/ZArith/BinInt.vo theories/ZArith/Zcompare.vo theories/ZArith/Zorder.vo theories/ZArith/Zeven.vo theories/ZArith/Zmin.vo theories/ZArith/Zabs.vo theories/ZArith/Znat.vo theories/ZArith/auxiliary.vo theories/ZArith/Zsyntax.vo theories/ZArith/ZArith_dec.vo theories/ZArith/Zbool.vo theories/ZArith/Zmisc.vo theories/ZArith/Wf_Z.vo theories/ZArith/Zhints.vo
-theories/ZArith/Zbool.vo: theories/ZArith/Zbool.v theories/ZArith/BinInt.vo theories/ZArith/Zeven.vo theories/ZArith/Zorder.vo theories/ZArith/Zcompare.vo theories/ZArith/ZArith_dec.vo theories/ZArith/Zsyntax.vo theories/Bool/Sumbool.vo
+theories/ZArith/ZArith_base.vo: theories/ZArith/ZArith_base.v theories/NArith/BinPos.vo theories/NArith/BinNat.vo theories/ZArith/BinInt.vo theories/ZArith/Zcompare.vo theories/ZArith/Zorder.vo theories/ZArith/Zeven.vo theories/ZArith/Zmin.vo theories/ZArith/Zabs.vo theories/ZArith/Znat.vo theories/ZArith/auxiliary.vo theories/ZArith/ZArith_dec.vo theories/ZArith/Zbool.vo theories/ZArith/Zmisc.vo theories/ZArith/Wf_Z.vo theories/ZArith/Zhints.vo
+theories/ZArith/Zbool.vo: theories/ZArith/Zbool.v theories/ZArith/BinInt.vo theories/ZArith/Zeven.vo theories/ZArith/Zorder.vo theories/ZArith/Zcompare.vo theories/ZArith/ZArith_dec.vo theories/Bool/Sumbool.vo
 theories/ZArith/Zbinary.vo: theories/ZArith/Zbinary.v theories/Bool/Bvector.vo theories/ZArith/ZArith.vo theories/ZArith/Zpower.vo contrib/omega/Omega.vo
 theories/ZArith/Znumtheory.vo: theories/ZArith/Znumtheory.v theories/ZArith/ZArith_base.vo contrib/ring/ZArithRing.vo theories/ZArith/Zcomplements.vo theories/ZArith/Zdiv.vo
 theories/Lists/MonoList.vo: theories/Lists/MonoList.v theories/Arith/Le.vo
-theories/Lists/PolyListSyntax.vo: theories/Lists/PolyListSyntax.v
-theories/Lists/ListSet.vo: theories/Lists/ListSet.v theories/Lists/PolyList.vo
+theories/Lists/ListSet.vo: theories/Lists/ListSet.v theories/Lists/List.vo
 theories/Lists/Streams.vo: theories/Lists/Streams.v
-theories/Lists/PolyList.vo: theories/Lists/PolyList.v theories/Arith/Le.vo
-theories/Lists/TheoryList.vo: theories/Lists/TheoryList.v theories/Lists/PolyList.vo theories/Arith/Le.vo theories/Arith/Lt.vo theories/Arith/Minus.vo theories/Bool/DecBool.vo
+theories/Lists/TheoryList.vo: theories/Lists/TheoryList.v theories/Lists/List.vo theories/Arith/Le.vo theories/Arith/Lt.vo theories/Arith/Minus.vo theories/Bool/DecBool.vo
 theories/Lists/List.vo: theories/Lists/List.v theories/Arith/Le.vo
 theories/Sets/Classical_sets.vo: theories/Sets/Classical_sets.v theories/Sets/Ensembles.vo theories/Sets/Constructive_sets.vo theories/Logic/Classical_Type.vo
 theories/Sets/Permut.vo: theories/Sets/Permut.v
@@ -173,31 +168,31 @@ theories/Sets/Relations_3_facts.vo: theories/Sets/Relations_3_facts.v theories/S
 theories/Sets/Partial_Order.vo: theories/Sets/Partial_Order.v theories/Sets/Ensembles.vo theories/Sets/Relations_1.vo
 theories/Sets/Uniset.vo: theories/Sets/Uniset.v theories/Bool/Bool.vo theories/Sets/Permut.vo
 theories/IntMap/Adalloc.vo: theories/IntMap/Adalloc.v theories/Bool/Bool.vo theories/Bool/Sumbool.vo theories/ZArith/ZArith.vo theories/Arith/Arith.vo theories/IntMap/Addr.vo theories/IntMap/Adist.vo theories/IntMap/Addec.vo theories/IntMap/Map.vo theories/IntMap/Fset.vo
-theories/IntMap/Mapcanon.vo: theories/IntMap/Mapcanon.v theories/Bool/Bool.vo theories/Bool/Sumbool.vo theories/Arith/Arith.vo theories/ZArith/ZArith.vo theories/IntMap/Addr.vo theories/IntMap/Adist.vo theories/IntMap/Addec.vo theories/IntMap/Map.vo theories/IntMap/Mapaxioms.vo theories/IntMap/Mapiter.vo theories/IntMap/Fset.vo theories/Lists/PolyList.vo theories/IntMap/Lsort.vo theories/IntMap/Mapsubset.vo theories/IntMap/Mapcard.vo
+theories/IntMap/Mapcanon.vo: theories/IntMap/Mapcanon.v theories/Bool/Bool.vo theories/Bool/Sumbool.vo theories/Arith/Arith.vo theories/ZArith/ZArith.vo theories/IntMap/Addr.vo theories/IntMap/Adist.vo theories/IntMap/Addec.vo theories/IntMap/Map.vo theories/IntMap/Mapaxioms.vo theories/IntMap/Mapiter.vo theories/IntMap/Fset.vo theories/Lists/List.vo theories/IntMap/Lsort.vo theories/IntMap/Mapsubset.vo theories/IntMap/Mapcard.vo
 theories/IntMap/Addec.vo: theories/IntMap/Addec.v theories/Bool/Bool.vo theories/Bool/Sumbool.vo theories/ZArith/ZArith.vo theories/IntMap/Addr.vo
-theories/IntMap/Mapcard.vo: theories/IntMap/Mapcard.v theories/Bool/Bool.vo theories/Bool/Sumbool.vo theories/Arith/Arith.vo theories/ZArith/ZArith.vo theories/IntMap/Addr.vo theories/IntMap/Adist.vo theories/IntMap/Addec.vo theories/IntMap/Map.vo theories/IntMap/Mapaxioms.vo theories/IntMap/Mapiter.vo theories/IntMap/Fset.vo theories/IntMap/Mapsubset.vo theories/Lists/PolyList.vo theories/IntMap/Lsort.vo theories/Arith/Peano_dec.vo
+theories/IntMap/Mapcard.vo: theories/IntMap/Mapcard.v theories/Bool/Bool.vo theories/Bool/Sumbool.vo theories/Arith/Arith.vo theories/ZArith/ZArith.vo theories/IntMap/Addr.vo theories/IntMap/Adist.vo theories/IntMap/Addec.vo theories/IntMap/Map.vo theories/IntMap/Mapaxioms.vo theories/IntMap/Mapiter.vo theories/IntMap/Fset.vo theories/IntMap/Mapsubset.vo theories/Lists/List.vo theories/IntMap/Lsort.vo theories/Arith/Peano_dec.vo
 theories/IntMap/Addr.vo: theories/IntMap/Addr.v theories/Bool/Bool.vo theories/ZArith/ZArith.vo
-theories/IntMap/Mapc.vo: theories/IntMap/Mapc.v theories/Bool/Bool.vo theories/Bool/Sumbool.vo theories/Arith/Arith.vo theories/ZArith/ZArith.vo theories/IntMap/Addr.vo theories/IntMap/Adist.vo theories/IntMap/Addec.vo theories/IntMap/Map.vo theories/IntMap/Mapaxioms.vo theories/IntMap/Fset.vo theories/IntMap/Mapiter.vo theories/IntMap/Mapsubset.vo theories/Lists/PolyList.vo theories/IntMap/Lsort.vo theories/IntMap/Mapcard.vo theories/IntMap/Mapcanon.vo
+theories/IntMap/Mapc.vo: theories/IntMap/Mapc.v theories/Bool/Bool.vo theories/Bool/Sumbool.vo theories/Arith/Arith.vo theories/ZArith/ZArith.vo theories/IntMap/Addr.vo theories/IntMap/Adist.vo theories/IntMap/Addec.vo theories/IntMap/Map.vo theories/IntMap/Mapaxioms.vo theories/IntMap/Fset.vo theories/IntMap/Mapiter.vo theories/IntMap/Mapsubset.vo theories/Lists/List.vo theories/IntMap/Lsort.vo theories/IntMap/Mapcard.vo theories/IntMap/Mapcanon.vo
 theories/IntMap/Adist.vo: theories/IntMap/Adist.v theories/Bool/Bool.vo theories/ZArith/ZArith.vo theories/Arith/Arith.vo theories/Arith/Min.vo theories/IntMap/Addr.vo
-theories/IntMap/Mapfold.vo: theories/IntMap/Mapfold.v theories/Bool/Bool.vo theories/Bool/Sumbool.vo theories/ZArith/ZArith.vo theories/IntMap/Addr.vo theories/IntMap/Adist.vo theories/IntMap/Addec.vo theories/IntMap/Map.vo theories/IntMap/Fset.vo theories/IntMap/Mapaxioms.vo theories/IntMap/Mapiter.vo theories/IntMap/Lsort.vo theories/IntMap/Mapsubset.vo theories/Lists/PolyList.vo
+theories/IntMap/Mapfold.vo: theories/IntMap/Mapfold.v theories/Bool/Bool.vo theories/Bool/Sumbool.vo theories/ZArith/ZArith.vo theories/IntMap/Addr.vo theories/IntMap/Adist.vo theories/IntMap/Addec.vo theories/IntMap/Map.vo theories/IntMap/Fset.vo theories/IntMap/Mapaxioms.vo theories/IntMap/Mapiter.vo theories/IntMap/Lsort.vo theories/IntMap/Mapsubset.vo theories/Lists/List.vo
 theories/IntMap/Allmaps.vo: theories/IntMap/Allmaps.v theories/IntMap/Addr.vo theories/IntMap/Adist.vo theories/IntMap/Addec.vo theories/IntMap/Map.vo theories/IntMap/Fset.vo theories/IntMap/Mapaxioms.vo theories/IntMap/Mapiter.vo theories/IntMap/Mapsubset.vo theories/IntMap/Lsort.vo theories/IntMap/Mapfold.vo theories/IntMap/Mapcard.vo theories/IntMap/Mapcanon.vo theories/IntMap/Mapc.vo theories/IntMap/Maplists.vo theories/IntMap/Adalloc.vo
-theories/IntMap/Mapiter.vo: theories/IntMap/Mapiter.v theories/Bool/Bool.vo theories/Bool/Sumbool.vo theories/ZArith/ZArith.vo theories/IntMap/Addr.vo theories/IntMap/Adist.vo theories/IntMap/Addec.vo theories/IntMap/Map.vo theories/IntMap/Mapaxioms.vo theories/IntMap/Fset.vo theories/Lists/PolyList.vo
+theories/IntMap/Mapiter.vo: theories/IntMap/Mapiter.v theories/Bool/Bool.vo theories/Bool/Sumbool.vo theories/ZArith/ZArith.vo theories/IntMap/Addr.vo theories/IntMap/Adist.vo theories/IntMap/Addec.vo theories/IntMap/Map.vo theories/IntMap/Mapaxioms.vo theories/IntMap/Fset.vo theories/Lists/List.vo
 theories/IntMap/Fset.vo: theories/IntMap/Fset.v theories/Bool/Bool.vo theories/Bool/Sumbool.vo theories/ZArith/ZArith.vo theories/IntMap/Addr.vo theories/IntMap/Adist.vo theories/IntMap/Addec.vo theories/IntMap/Map.vo
-theories/IntMap/Maplists.vo: theories/IntMap/Maplists.v theories/IntMap/Addr.vo theories/IntMap/Addec.vo theories/IntMap/Map.vo theories/IntMap/Fset.vo theories/IntMap/Mapaxioms.vo theories/IntMap/Mapsubset.vo theories/IntMap/Mapcard.vo theories/IntMap/Mapcanon.vo theories/IntMap/Mapc.vo theories/Bool/Bool.vo theories/Bool/Sumbool.vo theories/Lists/PolyList.vo theories/Arith/Arith.vo theories/IntMap/Mapiter.vo theories/IntMap/Mapfold.vo
-theories/IntMap/Lsort.vo: theories/IntMap/Lsort.v theories/Bool/Bool.vo theories/Bool/Sumbool.vo theories/Arith/Arith.vo theories/ZArith/ZArith.vo theories/IntMap/Addr.vo theories/IntMap/Adist.vo theories/IntMap/Addec.vo theories/IntMap/Map.vo theories/Lists/PolyList.vo theories/IntMap/Mapiter.vo
+theories/IntMap/Maplists.vo: theories/IntMap/Maplists.v theories/IntMap/Addr.vo theories/IntMap/Addec.vo theories/IntMap/Map.vo theories/IntMap/Fset.vo theories/IntMap/Mapaxioms.vo theories/IntMap/Mapsubset.vo theories/IntMap/Mapcard.vo theories/IntMap/Mapcanon.vo theories/IntMap/Mapc.vo theories/Bool/Bool.vo theories/Bool/Sumbool.vo theories/Lists/List.vo theories/Arith/Arith.vo theories/IntMap/Mapiter.vo theories/IntMap/Mapfold.vo
+theories/IntMap/Lsort.vo: theories/IntMap/Lsort.v theories/Bool/Bool.vo theories/Bool/Sumbool.vo theories/Arith/Arith.vo theories/ZArith/ZArith.vo theories/IntMap/Addr.vo theories/IntMap/Adist.vo theories/IntMap/Addec.vo theories/IntMap/Map.vo theories/Lists/List.vo theories/IntMap/Mapiter.vo
 theories/IntMap/Mapsubset.vo: theories/IntMap/Mapsubset.v theories/Bool/Bool.vo theories/Bool/Sumbool.vo theories/Arith/Arith.vo theories/ZArith/ZArith.vo theories/IntMap/Addr.vo theories/IntMap/Adist.vo theories/IntMap/Addec.vo theories/IntMap/Map.vo theories/IntMap/Fset.vo theories/IntMap/Mapaxioms.vo theories/IntMap/Mapiter.vo
 theories/IntMap/Mapaxioms.vo: theories/IntMap/Mapaxioms.v theories/Bool/Bool.vo theories/Bool/Sumbool.vo theories/ZArith/ZArith.vo theories/IntMap/Addr.vo theories/IntMap/Adist.vo theories/IntMap/Addec.vo theories/IntMap/Map.vo theories/IntMap/Fset.vo
 theories/IntMap/Map.vo: theories/IntMap/Map.v theories/Bool/Bool.vo theories/Bool/Sumbool.vo theories/ZArith/ZArith.vo theories/IntMap/Addr.vo theories/IntMap/Adist.vo theories/IntMap/Addec.vo
 theories/Relations/Newman.vo: theories/Relations/Newman.v theories/Relations/Rstar.vo
 theories/Relations/Operators_Properties.vo: theories/Relations/Operators_Properties.v theories/Relations/Relation_Definitions.vo theories/Relations/Relation_Operators.vo
 theories/Relations/Relation_Definitions.vo: theories/Relations/Relation_Definitions.v
-theories/Relations/Relation_Operators.vo: theories/Relations/Relation_Operators.v theories/Relations/Relation_Definitions.vo theories/Lists/PolyList.vo theories/Lists/PolyListSyntax.vo
+theories/Relations/Relation_Operators.vo: theories/Relations/Relation_Operators.v theories/Relations/Relation_Definitions.vo theories/Lists/List.vo
 theories/Relations/Relations.vo: theories/Relations/Relations.v theories/Relations/Relation_Definitions.vo theories/Relations/Relation_Operators.vo theories/Relations/Operators_Properties.vo
 theories/Relations/Rstar.vo: theories/Relations/Rstar.v
 theories/Wellfounded/Disjoint_Union.vo: theories/Wellfounded/Disjoint_Union.v theories/Relations/Relation_Operators.vo
 theories/Wellfounded/Inclusion.vo: theories/Wellfounded/Inclusion.v theories/Relations/Relation_Definitions.vo
 theories/Wellfounded/Inverse_Image.vo: theories/Wellfounded/Inverse_Image.v
-theories/Wellfounded/Lexicographic_Exponentiation.vo: theories/Wellfounded/Lexicographic_Exponentiation.v theories/Logic/Eqdep.vo theories/Lists/PolyList.vo theories/Lists/PolyListSyntax.vo theories/Relations/Relation_Operators.vo theories/Wellfounded/Transitive_Closure.vo
+theories/Wellfounded/Lexicographic_Exponentiation.vo: theories/Wellfounded/Lexicographic_Exponentiation.v theories/Logic/Eqdep.vo theories/Lists/List.vo theories/Relations/Relation_Operators.vo theories/Wellfounded/Transitive_Closure.vo
 theories/Wellfounded/Transitive_Closure.vo: theories/Wellfounded/Transitive_Closure.v theories/Relations/Relation_Definitions.vo theories/Relations/Relation_Operators.vo
 theories/Wellfounded/Union.vo: theories/Wellfounded/Union.v theories/Relations/Relation_Operators.vo theories/Relations/Relation_Definitions.vo theories/Wellfounded/Transitive_Closure.vo
 theories/Wellfounded/Wellfounded.vo: theories/Wellfounded/Wellfounded.v theories/Wellfounded/Disjoint_Union.vo theories/Wellfounded/Inclusion.vo theories/Wellfounded/Inverse_Image.vo theories/Wellfounded/Lexicographic_Exponentiation.vo theories/Wellfounded/Lexicographic_Product.vo theories/Wellfounded/Transitive_Closure.vo theories/Wellfounded/Union.vo theories/Wellfounded/Well_Ordering.vo
@@ -258,12 +253,12 @@ theories/Reals/RiemannInt.vo: theories/Reals/RiemannInt.v theories/Reals/Rfuncti
 theories/Reals/Integration.vo: theories/Reals/Integration.v theories/Reals/NewtonInt.vo theories/Reals/RiemannInt_SF.vo theories/Reals/RiemannInt.vo
 theories/Reals/Reals.vo: theories/Reals/Reals.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo.vo theories/Reals/Ranalysis.vo theories/Reals/Integration.vo
 theories/Setoids/Setoid.vo: theories/Setoids/Setoid.v
-theories/Sorting/Heap.vo: theories/Sorting/Heap.v theories/Lists/PolyList.vo theories/Sets/Multiset.vo theories/Sorting/Permutation.vo theories/Relations/Relations.vo theories/Sorting/Sorting.vo
-theories/Sorting/Permutation.vo: theories/Sorting/Permutation.v theories/Relations/Relations.vo theories/Lists/PolyList.vo theories/Sets/Multiset.vo
-theories/Sorting/Sorting.vo: theories/Sorting/Sorting.v theories/Lists/PolyList.vo theories/Sets/Multiset.vo theories/Sorting/Permutation.vo theories/Relations/Relations.vo
+theories/Sorting/Heap.vo: theories/Sorting/Heap.v theories/Lists/List.vo theories/Sets/Multiset.vo theories/Sorting/Permutation.vo theories/Relations/Relations.vo theories/Sorting/Sorting.vo
+theories/Sorting/Permutation.vo: theories/Sorting/Permutation.v theories/Relations/Relations.vo theories/Lists/List.vo theories/Sets/Multiset.vo
+theories/Sorting/Sorting.vo: theories/Sorting/Sorting.v theories/Lists/List.vo theories/Sets/Multiset.vo theories/Sorting/Permutation.vo theories/Relations/Relations.vo
 contrib/omega/OmegaLemmas.vo: contrib/omega/OmegaLemmas.v theories/ZArith/ZArith_base.vo
 contrib/omega/Omega.vo: contrib/omega/Omega.v theories/ZArith/ZArith_base.vo contrib/omega/OmegaLemmas.vo theories/ZArith/Zhints.vo
-contrib/romega/ReflOmegaCore.vo: contrib/romega/ReflOmegaCore.v theories/Arith/Arith.vo theories/Lists/PolyList.vo theories/Bool/Bool.vo theories/ZArith/ZArith_base.vo contrib/omega/OmegaLemmas.vo
+contrib/romega/ReflOmegaCore.vo: contrib/romega/ReflOmegaCore.v theories/Arith/Arith.vo theories/Lists/List.vo theories/Bool/Bool.vo theories/ZArith/ZArith_base.vo contrib/omega/OmegaLemmas.vo
 contrib/romega/ROmega.vo: contrib/romega/ROmega.v contrib/omega/Omega.vo contrib/romega/ReflOmegaCore.vo
 contrib/ring/ArithRing.vo: contrib/ring/ArithRing.v contrib/ring/Ring.vo theories/Arith/Arith.vo theories/Logic/Eqdep_dec.vo
 contrib/ring/Ring_normalize.vo: contrib/ring/Ring_normalize.v contrib/ring/Ring_theory.vo contrib/ring/Quote.vo
diff --git a/.depend.coq7 b/.depend.coq7
new file mode 100644
index 000000000..9a038ddb7
--- /dev/null
+++ b/.depend.coq7
@@ -0,0 +1,239 @@
+theories7/Init/Notations.vo: theories7/Init/Notations.v
+theories7/Init/Datatypes.vo: theories7/Init/Datatypes.v theories7/Init/Notations.vo theories7/Init/Logic.vo
+theories7/Init/Peano.vo: theories7/Init/Peano.v theories7/Init/Notations.vo theories7/Init/Datatypes.vo theories7/Init/Logic.vo
+theories7/Init/Logic.vo: theories7/Init/Logic.v theories7/Init/Notations.vo
+theories7/Init/Specif.vo: theories7/Init/Specif.v theories7/Init/Notations.vo theories7/Init/Datatypes.vo theories7/Init/Logic.vo
+theories7/Init/Logic_Type.vo: theories7/Init/Logic_Type.v theories7/Init/Datatypes.vo theories7/Init/Logic.vo
+theories7/Init/Wf.vo: theories7/Init/Wf.v theories7/Init/Notations.vo theories7/Init/Logic.vo theories7/Init/Datatypes.vo
+theories7/Init/Prelude.vo: theories7/Init/Prelude.v theories7/Init/Notations.vo theories7/Init/Logic.vo theories7/Init/Datatypes.vo theories7/Init/Specif.vo theories7/Init/Peano.vo theories7/Init/Wf.vo
+theories7/Init/Notations.vo: theories7/Init/Notations.v
+theories7/Init/Datatypes.vo: theories7/Init/Datatypes.v theories7/Init/Notations.vo theories7/Init/Logic.vo
+theories7/Init/Peano.vo: theories7/Init/Peano.v theories7/Init/Notations.vo theories7/Init/Datatypes.vo theories7/Init/Logic.vo
+theories7/Init/Logic.vo: theories7/Init/Logic.v theories7/Init/Notations.vo
+theories7/Init/Specif.vo: theories7/Init/Specif.v theories7/Init/Notations.vo theories7/Init/Datatypes.vo theories7/Init/Logic.vo
+theories7/Init/Logic_Type.vo: theories7/Init/Logic_Type.v theories7/Init/Datatypes.vo theories7/Init/Logic.vo
+theories7/Init/Wf.vo: theories7/Init/Wf.v theories7/Init/Notations.vo theories7/Init/Logic.vo theories7/Init/Datatypes.vo
+theories7/Init/Prelude.vo: theories7/Init/Prelude.v theories7/Init/Notations.vo theories7/Init/Logic.vo theories7/Init/Datatypes.vo theories7/Init/Specif.vo theories7/Init/Peano.vo theories7/Init/Wf.vo
+theories7/Logic/Hurkens.vo: theories7/Logic/Hurkens.v
+theories7/Logic/ProofIrrelevance.vo: theories7/Logic/ProofIrrelevance.v theories7/Logic/Hurkens.vo
+theories7/Logic/Classical.vo: theories7/Logic/Classical.v theories7/Logic/Classical_Prop.vo theories7/Logic/Classical_Pred_Type.vo
+theories7/Logic/Classical_Type.vo: theories7/Logic/Classical_Type.v theories7/Logic/Classical_Prop.vo theories7/Logic/Classical_Pred_Type.vo
+theories7/Logic/Classical_Pred_Set.vo: theories7/Logic/Classical_Pred_Set.v theories7/Logic/Classical_Prop.vo
+theories7/Logic/Eqdep.vo: theories7/Logic/Eqdep.v
+theories7/Logic/Classical_Pred_Type.vo: theories7/Logic/Classical_Pred_Type.v theories7/Logic/Classical_Prop.vo
+theories7/Logic/Classical_Prop.vo: theories7/Logic/Classical_Prop.v theories7/Logic/ProofIrrelevance.vo
+theories7/Logic/ClassicalFacts.vo: theories7/Logic/ClassicalFacts.v
+theories7/Logic/ChoiceFacts.vo: theories7/Logic/ChoiceFacts.v
+theories7/Logic/Berardi.vo: theories7/Logic/Berardi.v
+theories7/Logic/Eqdep_dec.vo: theories7/Logic/Eqdep_dec.v
+theories7/Logic/Decidable.vo: theories7/Logic/Decidable.v
+theories7/Logic/JMeq.vo: theories7/Logic/JMeq.v theories7/Logic/Eqdep.vo
+theories7/Logic/ClassicalDescription.vo: theories7/Logic/ClassicalDescription.v theories7/Logic/Classical.vo
+theories7/Logic/ClassicalChoice.vo: theories7/Logic/ClassicalChoice.v theories7/Logic/ClassicalDescription.vo theories7/Logic/RelationalChoice.vo theories7/Logic/ChoiceFacts.vo
+theories7/Logic/RelationalChoice.vo: theories7/Logic/RelationalChoice.v
+theories7/Logic/Diaconescu.vo: theories7/Logic/Diaconescu.v theories7/Logic/ClassicalFacts.vo theories7/Logic/ChoiceFacts.vo theories7/Bool/Bool.vo
+theories7/Arith/Arith.vo: theories7/Arith/Arith.v theories7/Arith/Le.vo theories7/Arith/Lt.vo theories7/Arith/Plus.vo theories7/Arith/Gt.vo theories7/Arith/Minus.vo theories7/Arith/Mult.vo theories7/Arith/Between.vo theories7/Arith/Peano_dec.vo theories7/Arith/Compare_dec.vo theories7/Arith/Factorial.vo
+theories7/Arith/Gt.vo: theories7/Arith/Gt.v theories7/Arith/Le.vo theories7/Arith/Lt.vo theories7/Arith/Plus.vo
+theories7/Arith/Between.vo: theories7/Arith/Between.v theories7/Arith/Le.vo theories7/Arith/Lt.vo
+theories7/Arith/Le.vo: theories7/Arith/Le.v
+theories7/Arith/Compare.vo: theories7/Arith/Compare.v theories7/Arith/Arith.vo theories7/Arith/Peano_dec.vo theories7/Arith/Compare_dec.vo theories7/Arith/Wf_nat.vo theories7/Arith/Min.vo
+theories7/Arith/Lt.vo: theories7/Arith/Lt.v theories7/Arith/Le.vo
+theories7/Arith/Compare_dec.vo: theories7/Arith/Compare_dec.v theories7/Arith/Le.vo theories7/Arith/Lt.vo theories7/Arith/Gt.vo theories7/Logic/Decidable.vo
+theories7/Arith/Min.vo: theories7/Arith/Min.v theories7/Arith/Arith.vo
+theories7/Arith/Div2.vo: theories7/Arith/Div2.v theories7/Arith/Lt.vo theories7/Arith/Plus.vo theories7/Arith/Compare_dec.vo theories7/Arith/Even.vo
+theories7/Arith/Minus.vo: theories7/Arith/Minus.v theories7/Arith/Lt.vo theories7/Arith/Le.vo
+theories7/Arith/Mult.vo: theories7/Arith/Mult.v theories7/Arith/Plus.vo theories7/Arith/Minus.vo theories7/Arith/Lt.vo theories7/Arith/Le.vo
+theories7/Arith/Even.vo: theories7/Arith/Even.v
+theories7/Arith/EqNat.vo: theories7/Arith/EqNat.v
+theories7/Arith/Peano_dec.vo: theories7/Arith/Peano_dec.v theories7/Logic/Decidable.vo
+theories7/Arith/Euclid.vo: theories7/Arith/Euclid.v theories7/Arith/Mult.vo theories7/Arith/Compare_dec.vo theories7/Arith/Wf_nat.vo
+theories7/Arith/Plus.vo: theories7/Arith/Plus.v theories7/Arith/Le.vo theories7/Arith/Lt.vo
+theories7/Arith/Wf_nat.vo: theories7/Arith/Wf_nat.v theories7/Arith/Lt.vo
+theories7/Arith/Max.vo: theories7/Arith/Max.v theories7/Arith/Arith.vo
+theories7/Arith/Bool_nat.vo: theories7/Arith/Bool_nat.v theories7/Arith/Compare_dec.vo theories7/Arith/Peano_dec.vo theories7/Bool/Sumbool.vo
+theories7/Arith/Factorial.vo: theories7/Arith/Factorial.v theories7/Arith/Plus.vo theories7/Arith/Mult.vo theories7/Arith/Lt.vo
+theories7/Bool/Bool.vo: theories7/Bool/Bool.v
+theories7/Bool/IfProp.vo: theories7/Bool/IfProp.v theories7/Bool/Bool.vo
+theories7/Bool/Zerob.vo: theories7/Bool/Zerob.v theories7/Arith/Arith.vo theories7/Bool/Bool.vo
+theories7/Bool/DecBool.vo: theories7/Bool/DecBool.v
+theories7/Bool/Sumbool.vo: theories7/Bool/Sumbool.v
+theories7/Bool/BoolEq.vo: theories7/Bool/BoolEq.v theories7/Bool/Bool.vo
+theories7/Bool/Bvector.vo: theories7/Bool/Bvector.v theories7/Bool/Bool.vo theories7/Bool/Sumbool.vo theories7/Arith/Arith.vo
+theories7/NArith/BinPos.vo: theories7/NArith/BinPos.v
+theories7/NArith/Pnat.vo: theories7/NArith/Pnat.v theories7/NArith/BinPos.vo theories7/Arith/Le.vo theories7/Arith/Lt.vo theories7/Arith/Gt.vo theories7/Arith/Plus.vo theories7/Arith/Mult.vo theories7/Arith/Minus.vo
+theories7/NArith/BinNat.vo: theories7/NArith/BinNat.v theories7/NArith/BinPos.vo
+theories7/NArith/NArith.vo: theories7/NArith/NArith.v theories7/NArith/BinPos.vo theories7/NArith/BinNat.vo
+theories7/ZArith/BinInt.vo: theories7/ZArith/BinInt.v theories7/NArith/BinPos.vo theories7/NArith/Pnat.vo theories7/NArith/BinNat.vo theories7/Arith/Plus.vo theories7/Arith/Mult.vo
+theories7/ZArith/Wf_Z.vo: theories7/ZArith/Wf_Z.v theories7/ZArith/BinInt.vo theories7/ZArith/Zcompare.vo theories7/ZArith/Zorder.vo theories7/ZArith/Znat.vo theories7/ZArith/Zmisc.vo theories7/ZArith/Zsyntax.vo theories7/Arith/Wf_nat.vo
+theories7/ZArith/ZArith.vo: theories7/ZArith/ZArith.v theories7/ZArith/ZArith_base.vo theories7/ZArith/Zcomplements.vo theories7/ZArith/Zsqrt.vo theories7/ZArith/Zpower.vo theories7/ZArith/Zdiv.vo theories7/ZArith/Zlogarithm.vo theories7/ZArith/Zbool.vo
+theories7/ZArith/ZArith_dec.vo: theories7/ZArith/ZArith_dec.v theories7/Bool/Sumbool.vo theories7/ZArith/BinInt.vo theories7/ZArith/Zorder.vo theories7/ZArith/Zcompare.vo theories7/ZArith/Zsyntax.vo
+theories7/ZArith/auxiliary.vo: theories7/ZArith/auxiliary.v theories7/Arith/Arith.vo theories7/ZArith/BinInt.vo theories7/ZArith/Zorder.vo theories7/Logic/Decidable.vo theories7/Arith/Peano_dec.vo theories7/Arith/Compare_dec.vo theories7/ZArith/Znat.vo theories7/ZArith/Zcompare.vo
+theories7/ZArith/Zmisc.vo: theories7/ZArith/Zmisc.v theories7/ZArith/BinInt.vo theories7/ZArith/Zcompare.vo theories7/ZArith/Zorder.vo theories7/ZArith/Zsyntax.vo theories7/Bool/Bool.vo theories7/ZArith/Zbool.vo theories7/ZArith/Zeven.vo theories7/ZArith/Zabs.vo theories7/ZArith/Zmin.vo
+theories7/ZArith/Zcompare.vo: theories7/ZArith/Zcompare.v theories7/NArith/BinPos.vo theories7/ZArith/BinInt.vo theories7/ZArith/Zsyntax.vo theories7/Arith/Lt.vo theories7/Arith/Gt.vo theories7/Arith/Plus.vo theories7/Arith/Mult.vo
+theories7/ZArith/Znat.vo: theories7/ZArith/Znat.v theories7/Arith/Arith.vo theories7/NArith/BinPos.vo theories7/ZArith/BinInt.vo theories7/ZArith/Zcompare.vo theories7/ZArith/Zorder.vo theories7/Logic/Decidable.vo theories7/Arith/Peano_dec.vo theories7/Arith/Compare_dec.vo
+theories7/ZArith/Zorder.vo: theories7/ZArith/Zorder.v theories7/NArith/BinPos.vo theories7/ZArith/BinInt.vo theories7/Arith/Arith.vo theories7/Logic/Decidable.vo theories7/ZArith/Zsyntax.vo theories7/ZArith/Zcompare.vo
+theories7/ZArith/Zabs.vo: theories7/ZArith/Zabs.v theories7/Arith/Arith.vo theories7/NArith/BinPos.vo theories7/ZArith/BinInt.vo theories7/ZArith/Zorder.vo theories7/ZArith/Zsyntax.vo theories7/ZArith/ZArith_dec.vo
+theories7/ZArith/Zmin.vo: theories7/ZArith/Zmin.v theories7/Arith/Arith.vo theories7/ZArith/BinInt.vo theories7/ZArith/Zcompare.vo theories7/ZArith/Zorder.vo
+theories7/ZArith/Zeven.vo: theories7/ZArith/Zeven.v theories7/ZArith/BinInt.vo theories7/ZArith/Zsyntax.vo
+theories7/ZArith/Zhints.vo: theories7/ZArith/Zhints.v theories7/ZArith/BinInt.vo theories7/ZArith/Zorder.vo theories7/ZArith/Zmin.vo theories7/ZArith/Zabs.vo theories7/ZArith/Zcompare.vo theories7/ZArith/Znat.vo theories7/ZArith/auxiliary.vo theories7/ZArith/Zsyntax.vo theories7/ZArith/Zmisc.vo theories7/ZArith/Wf_Z.vo
+theories7/ZArith/Zlogarithm.vo: theories7/ZArith/Zlogarithm.v theories7/ZArith/ZArith_base.vo contrib7/omega/Omega.vo theories7/ZArith/Zcomplements.vo theories7/ZArith/Zpower.vo
+theories7/ZArith/Zpower.vo: theories7/ZArith/Zpower.v theories7/ZArith/ZArith_base.vo contrib7/omega/Omega.vo theories7/ZArith/Zcomplements.vo
+theories7/ZArith/Zcomplements.vo: theories7/ZArith/Zcomplements.v contrib7/ring/ZArithRing.vo theories7/ZArith/ZArith_base.vo contrib7/omega/Omega.vo theories7/Arith/Wf_nat.vo theories7/Lists/PolyList.vo
+theories7/ZArith/Zdiv.vo: theories7/ZArith/Zdiv.v theories7/ZArith/ZArith_base.vo theories7/ZArith/Zbool.vo contrib7/omega/Omega.vo contrib7/ring/ZArithRing.vo theories7/ZArith/Zcomplements.vo
+theories7/ZArith/Zsqrt.vo: theories7/ZArith/Zsqrt.v contrib7/omega/Omega.vo theories7/ZArith/ZArith_base.vo contrib7/ring/ZArithRing.vo
+theories7/ZArith/Zwf.vo: theories7/ZArith/Zwf.v theories7/ZArith/ZArith_base.vo theories7/Arith/Wf_nat.vo contrib7/omega/Omega.vo
+theories7/ZArith/ZArith_base.vo: theories7/ZArith/ZArith_base.v theories7/ZArith/fast_integer.vo theories7/ZArith/zarith_aux.vo theories7/NArith/BinPos.vo theories7/NArith/BinNat.vo theories7/ZArith/BinInt.vo theories7/ZArith/Zcompare.vo theories7/ZArith/Zorder.vo theories7/ZArith/Zeven.vo theories7/ZArith/Zmin.vo theories7/ZArith/Zabs.vo theories7/ZArith/Znat.vo theories7/ZArith/auxiliary.vo theories7/ZArith/Zsyntax.vo theories7/ZArith/ZArith_dec.vo theories7/ZArith/Zbool.vo theories7/ZArith/Zmisc.vo theories7/ZArith/Wf_Z.vo theories7/ZArith/Zhints.vo
+theories7/ZArith/Zbool.vo: theories7/ZArith/Zbool.v theories7/ZArith/BinInt.vo theories7/ZArith/Zeven.vo theories7/ZArith/Zorder.vo theories7/ZArith/Zcompare.vo theories7/ZArith/ZArith_dec.vo theories7/ZArith/Zsyntax.vo theories7/Bool/Sumbool.vo
+theories7/ZArith/Zbinary.vo: theories7/ZArith/Zbinary.v theories7/Bool/Bvector.vo theories7/ZArith/ZArith.vo theories7/ZArith/Zpower.vo contrib7/omega/Omega.vo
+theories7/ZArith/Znumtheory.vo: theories7/ZArith/Znumtheory.v theories7/ZArith/ZArith_base.vo contrib7/ring/ZArithRing.vo theories7/ZArith/Zcomplements.vo theories7/ZArith/Zdiv.vo
+theories7/Lists/MonoList.vo: theories7/Lists/MonoList.v theories7/Arith/Le.vo
+theories7/Lists/ListSet.vo: theories7/Lists/ListSet.v theories7/Lists/PolyList.vo
+theories7/Lists/Streams.vo: theories7/Lists/Streams.v
+theories7/Lists/TheoryList.vo: theories7/Lists/TheoryList.v theories7/Lists/PolyList.vo theories7/Arith/Le.vo theories7/Arith/Lt.vo theories7/Arith/Minus.vo theories7/Bool/DecBool.vo
+theories7/Lists/List.vo: theories7/Lists/List.v theories7/Arith/Le.vo
+theories7/Sets/Classical_sets.vo: theories7/Sets/Classical_sets.v theories7/Sets/Ensembles.vo theories7/Sets/Constructive_sets.vo theories7/Logic/Classical_Type.vo
+theories7/Sets/Permut.vo: theories7/Sets/Permut.v
+theories7/Sets/Constructive_sets.vo: theories7/Sets/Constructive_sets.v theories7/Sets/Ensembles.vo
+theories7/Sets/Powerset.vo: theories7/Sets/Powerset.v theories7/Sets/Ensembles.vo theories7/Sets/Relations_1.vo theories7/Sets/Relations_1_facts.vo theories7/Sets/Partial_Order.vo theories7/Sets/Cpo.vo
+theories7/Sets/Cpo.vo: theories7/Sets/Cpo.v theories7/Sets/Ensembles.vo theories7/Sets/Relations_1.vo theories7/Sets/Partial_Order.vo
+theories7/Sets/Powerset_Classical_facts.vo: theories7/Sets/Powerset_Classical_facts.v theories7/Sets/Ensembles.vo theories7/Sets/Constructive_sets.vo theories7/Sets/Relations_1.vo theories7/Sets/Relations_1_facts.vo theories7/Sets/Partial_Order.vo theories7/Sets/Cpo.vo theories7/Sets/Powerset.vo theories7/Sets/Powerset_facts.vo theories7/Logic/Classical_Type.vo theories7/Sets/Classical_sets.vo
+theories7/Sets/Ensembles.vo: theories7/Sets/Ensembles.v
+theories7/Sets/Powerset_facts.vo: theories7/Sets/Powerset_facts.v theories7/Sets/Ensembles.vo theories7/Sets/Constructive_sets.vo theories7/Sets/Relations_1.vo theories7/Sets/Relations_1_facts.vo theories7/Sets/Partial_Order.vo theories7/Sets/Cpo.vo theories7/Sets/Powerset.vo
+theories7/Sets/Finite_sets.vo: theories7/Sets/Finite_sets.v theories7/Sets/Ensembles.vo theories7/Sets/Constructive_sets.vo
+theories7/Sets/Relations_1.vo: theories7/Sets/Relations_1.v
+theories7/Sets/Finite_sets_facts.vo: theories7/Sets/Finite_sets_facts.v theories7/Sets/Finite_sets.vo theories7/Sets/Constructive_sets.vo theories7/Logic/Classical_Type.vo theories7/Sets/Classical_sets.vo theories7/Sets/Powerset.vo theories7/Sets/Powerset_facts.vo theories7/Sets/Powerset_Classical_facts.vo theories7/Arith/Gt.vo theories7/Arith/Lt.vo
+theories7/Sets/Relations_1_facts.vo: theories7/Sets/Relations_1_facts.v theories7/Sets/Relations_1.vo
+theories7/Sets/Image.vo: theories7/Sets/Image.v theories7/Sets/Finite_sets.vo theories7/Sets/Constructive_sets.vo theories7/Logic/Classical_Type.vo theories7/Sets/Classical_sets.vo theories7/Sets/Powerset.vo theories7/Sets/Powerset_facts.vo theories7/Sets/Powerset_Classical_facts.vo theories7/Arith/Gt.vo theories7/Arith/Lt.vo theories7/Arith/Le.vo theories7/Sets/Finite_sets_facts.vo
+theories7/Sets/Relations_2.vo: theories7/Sets/Relations_2.v theories7/Sets/Relations_1.vo
+theories7/Sets/Infinite_sets.vo: theories7/Sets/Infinite_sets.v theories7/Sets/Finite_sets.vo theories7/Sets/Constructive_sets.vo theories7/Logic/Classical_Type.vo theories7/Sets/Classical_sets.vo theories7/Sets/Powerset.vo theories7/Sets/Powerset_facts.vo theories7/Sets/Powerset_Classical_facts.vo theories7/Arith/Gt.vo theories7/Arith/Lt.vo theories7/Arith/Le.vo theories7/Sets/Finite_sets_facts.vo theories7/Sets/Image.vo
+theories7/Sets/Relations_2_facts.vo: theories7/Sets/Relations_2_facts.v theories7/Sets/Relations_1.vo theories7/Sets/Relations_1_facts.vo theories7/Sets/Relations_2.vo
+theories7/Sets/Integers.vo: theories7/Sets/Integers.v theories7/Sets/Finite_sets.vo theories7/Sets/Constructive_sets.vo theories7/Logic/Classical_Type.vo theories7/Sets/Classical_sets.vo theories7/Sets/Powerset.vo theories7/Sets/Powerset_facts.vo theories7/Sets/Powerset_Classical_facts.vo theories7/Arith/Gt.vo theories7/Arith/Lt.vo theories7/Arith/Le.vo theories7/Sets/Finite_sets_facts.vo theories7/Sets/Image.vo theories7/Sets/Infinite_sets.vo theories7/Arith/Compare_dec.vo theories7/Sets/Relations_1.vo theories7/Sets/Partial_Order.vo theories7/Sets/Cpo.vo
+theories7/Sets/Relations_3.vo: theories7/Sets/Relations_3.v theories7/Sets/Relations_1.vo theories7/Sets/Relations_2.vo
+theories7/Sets/Multiset.vo: theories7/Sets/Multiset.v theories7/Sets/Permut.vo theories7/Arith/Plus.vo
+theories7/Sets/Relations_3_facts.vo: theories7/Sets/Relations_3_facts.v theories7/Sets/Relations_1.vo theories7/Sets/Relations_1_facts.vo theories7/Sets/Relations_2.vo theories7/Sets/Relations_2_facts.vo theories7/Sets/Relations_3.vo
+theories7/Sets/Partial_Order.vo: theories7/Sets/Partial_Order.v theories7/Sets/Ensembles.vo theories7/Sets/Relations_1.vo
+theories7/Sets/Uniset.vo: theories7/Sets/Uniset.v theories7/Bool/Bool.vo theories7/Sets/Permut.vo
+theories7/IntMap/Adalloc.vo: theories7/IntMap/Adalloc.v theories7/Bool/Bool.vo theories7/Bool/Sumbool.vo theories7/ZArith/ZArith.vo theories7/Arith/Arith.vo theories7/IntMap/Addr.vo theories7/IntMap/Adist.vo theories7/IntMap/Addec.vo theories7/IntMap/Map.vo theories7/IntMap/Fset.vo
+theories7/IntMap/Mapcanon.vo: theories7/IntMap/Mapcanon.v theories7/Bool/Bool.vo theories7/Bool/Sumbool.vo theories7/Arith/Arith.vo theories7/ZArith/ZArith.vo theories7/IntMap/Addr.vo theories7/IntMap/Adist.vo theories7/IntMap/Addec.vo theories7/IntMap/Map.vo theories7/IntMap/Mapaxioms.vo theories7/IntMap/Mapiter.vo theories7/IntMap/Fset.vo theories7/Lists/PolyList.vo theories7/IntMap/Lsort.vo theories7/IntMap/Mapsubset.vo theories7/IntMap/Mapcard.vo
+theories7/IntMap/Addec.vo: theories7/IntMap/Addec.v theories7/Bool/Bool.vo theories7/Bool/Sumbool.vo theories7/ZArith/ZArith.vo theories7/IntMap/Addr.vo
+theories7/IntMap/Mapcard.vo: theories7/IntMap/Mapcard.v theories7/Bool/Bool.vo theories7/Bool/Sumbool.vo theories7/Arith/Arith.vo theories7/ZArith/ZArith.vo theories7/IntMap/Addr.vo theories7/IntMap/Adist.vo theories7/IntMap/Addec.vo theories7/IntMap/Map.vo theories7/IntMap/Mapaxioms.vo theories7/IntMap/Mapiter.vo theories7/IntMap/Fset.vo theories7/IntMap/Mapsubset.vo theories7/Lists/PolyList.vo theories7/IntMap/Lsort.vo theories7/Arith/Peano_dec.vo
+theories7/IntMap/Addr.vo: theories7/IntMap/Addr.v theories7/Bool/Bool.vo theories7/ZArith/ZArith.vo
+theories7/IntMap/Mapc.vo: theories7/IntMap/Mapc.v theories7/Bool/Bool.vo theories7/Bool/Sumbool.vo theories7/Arith/Arith.vo theories7/ZArith/ZArith.vo theories7/IntMap/Addr.vo theories7/IntMap/Adist.vo theories7/IntMap/Addec.vo theories7/IntMap/Map.vo theories7/IntMap/Mapaxioms.vo theories7/IntMap/Fset.vo theories7/IntMap/Mapiter.vo theories7/IntMap/Mapsubset.vo theories7/Lists/PolyList.vo theories7/IntMap/Lsort.vo theories7/IntMap/Mapcard.vo theories7/IntMap/Mapcanon.vo
+theories7/IntMap/Adist.vo: theories7/IntMap/Adist.v theories7/Bool/Bool.vo theories7/ZArith/ZArith.vo theories7/Arith/Arith.vo theories7/Arith/Min.vo theories7/IntMap/Addr.vo
+theories7/IntMap/Mapfold.vo: theories7/IntMap/Mapfold.v theories7/Bool/Bool.vo theories7/Bool/Sumbool.vo theories7/ZArith/ZArith.vo theories7/IntMap/Addr.vo theories7/IntMap/Adist.vo theories7/IntMap/Addec.vo theories7/IntMap/Map.vo theories7/IntMap/Fset.vo theories7/IntMap/Mapaxioms.vo theories7/IntMap/Mapiter.vo theories7/IntMap/Lsort.vo theories7/IntMap/Mapsubset.vo theories7/Lists/PolyList.vo
+theories7/IntMap/Allmaps.vo: theories7/IntMap/Allmaps.v theories7/IntMap/Addr.vo theories7/IntMap/Adist.vo theories7/IntMap/Addec.vo theories7/IntMap/Map.vo theories7/IntMap/Fset.vo theories7/IntMap/Mapaxioms.vo theories7/IntMap/Mapiter.vo theories7/IntMap/Mapsubset.vo theories7/IntMap/Lsort.vo theories7/IntMap/Mapfold.vo theories7/IntMap/Mapcard.vo theories7/IntMap/Mapcanon.vo theories7/IntMap/Mapc.vo theories7/IntMap/Maplists.vo theories7/IntMap/Adalloc.vo
+theories7/IntMap/Mapiter.vo: theories7/IntMap/Mapiter.v theories7/Bool/Bool.vo theories7/Bool/Sumbool.vo theories7/ZArith/ZArith.vo theories7/IntMap/Addr.vo theories7/IntMap/Adist.vo theories7/IntMap/Addec.vo theories7/IntMap/Map.vo theories7/IntMap/Mapaxioms.vo theories7/IntMap/Fset.vo theories7/Lists/PolyList.vo
+theories7/IntMap/Fset.vo: theories7/IntMap/Fset.v theories7/Bool/Bool.vo theories7/Bool/Sumbool.vo theories7/ZArith/ZArith.vo theories7/IntMap/Addr.vo theories7/IntMap/Adist.vo theories7/IntMap/Addec.vo theories7/IntMap/Map.vo
+theories7/IntMap/Maplists.vo: theories7/IntMap/Maplists.v theories7/IntMap/Addr.vo theories7/IntMap/Addec.vo theories7/IntMap/Map.vo theories7/IntMap/Fset.vo theories7/IntMap/Mapaxioms.vo theories7/IntMap/Mapsubset.vo theories7/IntMap/Mapcard.vo theories7/IntMap/Mapcanon.vo theories7/IntMap/Mapc.vo theories7/Bool/Bool.vo theories7/Bool/Sumbool.vo theories7/Lists/PolyList.vo theories7/Arith/Arith.vo theories7/IntMap/Mapiter.vo theories7/IntMap/Mapfold.vo
+theories7/IntMap/Lsort.vo: theories7/IntMap/Lsort.v theories7/Bool/Bool.vo theories7/Bool/Sumbool.vo theories7/Arith/Arith.vo theories7/ZArith/ZArith.vo theories7/IntMap/Addr.vo theories7/IntMap/Adist.vo theories7/IntMap/Addec.vo theories7/IntMap/Map.vo theories7/Lists/PolyList.vo theories7/IntMap/Mapiter.vo
+theories7/IntMap/Mapsubset.vo: theories7/IntMap/Mapsubset.v theories7/Bool/Bool.vo theories7/Bool/Sumbool.vo theories7/Arith/Arith.vo theories7/ZArith/ZArith.vo theories7/IntMap/Addr.vo theories7/IntMap/Adist.vo theories7/IntMap/Addec.vo theories7/IntMap/Map.vo theories7/IntMap/Fset.vo theories7/IntMap/Mapaxioms.vo theories7/IntMap/Mapiter.vo
+theories7/IntMap/Mapaxioms.vo: theories7/IntMap/Mapaxioms.v theories7/Bool/Bool.vo theories7/Bool/Sumbool.vo theories7/ZArith/ZArith.vo theories7/IntMap/Addr.vo theories7/IntMap/Adist.vo theories7/IntMap/Addec.vo theories7/IntMap/Map.vo theories7/IntMap/Fset.vo
+theories7/IntMap/Map.vo: theories7/IntMap/Map.v theories7/Bool/Bool.vo theories7/Bool/Sumbool.vo theories7/ZArith/ZArith.vo theories7/IntMap/Addr.vo theories7/IntMap/Adist.vo theories7/IntMap/Addec.vo
+theories7/Relations/Newman.vo: theories7/Relations/Newman.v theories7/Relations/Rstar.vo
+theories7/Relations/Operators_Properties.vo: theories7/Relations/Operators_Properties.v theories7/Relations/Relation_Definitions.vo theories7/Relations/Relation_Operators.vo
+theories7/Relations/Relation_Definitions.vo: theories7/Relations/Relation_Definitions.v
+theories7/Relations/Relation_Operators.vo: theories7/Relations/Relation_Operators.v theories7/Relations/Relation_Definitions.vo theories7/Lists/PolyList.vo theories7/Lists/PolyListSyntax.vo
+theories7/Relations/Relations.vo: theories7/Relations/Relations.v theories7/Relations/Relation_Definitions.vo theories7/Relations/Relation_Operators.vo theories7/Relations/Operators_Properties.vo
+theories7/Relations/Rstar.vo: theories7/Relations/Rstar.v
+theories7/Wellfounded/Disjoint_Union.vo: theories7/Wellfounded/Disjoint_Union.v theories7/Relations/Relation_Operators.vo
+theories7/Wellfounded/Inclusion.vo: theories7/Wellfounded/Inclusion.v theories7/Relations/Relation_Definitions.vo
+theories7/Wellfounded/Inverse_Image.vo: theories7/Wellfounded/Inverse_Image.v
+theories7/Wellfounded/Lexicographic_Exponentiation.vo: theories7/Wellfounded/Lexicographic_Exponentiation.v theories7/Logic/Eqdep.vo theories7/Lists/PolyList.vo theories7/Lists/PolyListSyntax.vo theories7/Relations/Relation_Operators.vo theories7/Wellfounded/Transitive_Closure.vo
+theories7/Wellfounded/Transitive_Closure.vo: theories7/Wellfounded/Transitive_Closure.v theories7/Relations/Relation_Definitions.vo theories7/Relations/Relation_Operators.vo
+theories7/Wellfounded/Union.vo: theories7/Wellfounded/Union.v theories7/Relations/Relation_Operators.vo theories7/Relations/Relation_Definitions.vo theories7/Wellfounded/Transitive_Closure.vo
+theories7/Wellfounded/Wellfounded.vo: theories7/Wellfounded/Wellfounded.v theories7/Wellfounded/Disjoint_Union.vo theories7/Wellfounded/Inclusion.vo theories7/Wellfounded/Inverse_Image.vo theories7/Wellfounded/Lexicographic_Exponentiation.vo theories7/Wellfounded/Lexicographic_Product.vo theories7/Wellfounded/Transitive_Closure.vo theories7/Wellfounded/Union.vo theories7/Wellfounded/Well_Ordering.vo
+theories7/Wellfounded/Well_Ordering.vo: theories7/Wellfounded/Well_Ordering.v theories7/Logic/Eqdep.vo
+theories7/Wellfounded/Lexicographic_Product.vo: theories7/Wellfounded/Lexicographic_Product.v theories7/Logic/Eqdep.vo theories7/Relations/Relation_Operators.vo theories7/Wellfounded/Transitive_Closure.vo
+theories7/Reals/Rdefinitions.vo: theories7/Reals/Rdefinitions.v theories7/ZArith/ZArith_base.vo
+theories7/Reals/Rsyntax.vo: theories7/Reals/Rsyntax.v theories7/Reals/Rdefinitions.vo
+theories7/Reals/Raxioms.vo: theories7/Reals/Raxioms.v theories7/ZArith/ZArith_base.vo theories7/Reals/Rsyntax.vo
+theories7/Reals/RIneq.vo: theories7/Reals/RIneq.v theories7/Reals/Raxioms.vo contrib7/ring/ZArithRing.vo contrib7/omega/Omega.vo contrib7/field/Field.vo
+theories7/Reals/DiscrR.vo: theories7/Reals/DiscrR.v theories7/Reals/RIneq.vo contrib7/omega/Omega.vo
+theories7/Reals/Rbase.vo: theories7/Reals/Rbase.v theories7/Reals/Rdefinitions.vo theories7/Reals/Raxioms.vo theories7/Reals/RIneq.vo theories7/Reals/DiscrR.vo
+theories7/Reals/R_Ifp.vo: theories7/Reals/R_Ifp.v theories7/Reals/Rbase.vo contrib7/omega/Omega.vo
+theories7/Reals/Rbasic_fun.vo: theories7/Reals/Rbasic_fun.v theories7/Reals/Rbase.vo theories7/Reals/R_Ifp.vo contrib7/fourier/Fourier.vo
+theories7/Reals/R_sqr.vo: theories7/Reals/R_sqr.v theories7/Reals/Rbase.vo theories7/Reals/Rbasic_fun.vo
+theories7/Reals/SplitAbsolu.vo: theories7/Reals/SplitAbsolu.v theories7/Reals/Rbasic_fun.vo
+theories7/Reals/SplitRmult.vo: theories7/Reals/SplitRmult.v theories7/Reals/Rbase.vo
+theories7/Reals/ArithProp.vo: theories7/Reals/ArithProp.v theories7/Reals/Rbase.vo theories7/Reals/Rbasic_fun.vo theories7/Arith/Even.vo theories7/Arith/Div2.vo
+theories7/Reals/Rfunctions.vo: theories7/Reals/Rfunctions.v theories7/Reals/Rbase.vo theories7/Reals/R_Ifp.vo theories7/Reals/Rbasic_fun.vo theories7/Reals/R_sqr.vo theories7/Reals/SplitAbsolu.vo theories7/Reals/SplitRmult.vo theories7/Reals/ArithProp.vo contrib7/omega/Omega.vo theories7/ZArith/Zpower.vo
+theories7/Reals/Rseries.vo: theories7/Reals/Rseries.v theories7/Reals/Rbase.vo theories7/Reals/Rfunctions.vo theories7/Logic/Classical.vo theories7/Arith/Compare.vo
+theories7/Reals/SeqProp.vo: theories7/Reals/SeqProp.v theories7/Reals/Rbase.vo theories7/Reals/Rfunctions.vo theories7/Reals/Rseries.vo theories7/Logic/Classical.vo theories7/Arith/Max.vo
+theories7/Reals/Rcomplete.vo: theories7/Reals/Rcomplete.v theories7/Reals/Rbase.vo theories7/Reals/Rfunctions.vo theories7/Reals/Rseries.vo theories7/Reals/SeqProp.vo theories7/Arith/Max.vo
+theories7/Reals/PartSum.vo: theories7/Reals/PartSum.v theories7/Reals/Rbase.vo theories7/Reals/Rfunctions.vo theories7/Reals/Rseries.vo theories7/Reals/Rcomplete.vo theories7/Arith/Max.vo
+theories7/Reals/AltSeries.vo: theories7/Reals/AltSeries.v theories7/Reals/Rbase.vo theories7/Reals/Rfunctions.vo theories7/Reals/Rseries.vo theories7/Reals/SeqProp.vo theories7/Reals/PartSum.vo theories7/Arith/Max.vo
+theories7/Reals/Binomial.vo: theories7/Reals/Binomial.v theories7/Reals/Rbase.vo theories7/Reals/Rfunctions.vo theories7/Reals/PartSum.vo
+theories7/Reals/Rsigma.vo: theories7/Reals/Rsigma.v theories7/Reals/Rbase.vo theories7/Reals/Rfunctions.vo theories7/Reals/Rseries.vo theories7/Reals/PartSum.vo
+theories7/Reals/Rprod.vo: theories7/Reals/Rprod.v theories7/Arith/Compare.vo theories7/Reals/Rbase.vo theories7/Reals/Rfunctions.vo theories7/Reals/Rseries.vo theories7/Reals/PartSum.vo theories7/Reals/Binomial.vo
+theories7/Reals/Cauchy_prod.vo: theories7/Reals/Cauchy_prod.v theories7/Reals/Rbase.vo theories7/Reals/Rfunctions.vo theories7/Reals/Rseries.vo theories7/Reals/PartSum.vo
+theories7/Reals/Alembert.vo: theories7/Reals/Alembert.v theories7/Reals/Rbase.vo theories7/Reals/Rfunctions.vo theories7/Reals/Rseries.vo theories7/Reals/SeqProp.vo theories7/Reals/PartSum.vo theories7/Arith/Max.vo
+theories7/Reals/SeqSeries.vo: theories7/Reals/SeqSeries.v theories7/Reals/Rbase.vo theories7/Reals/Rfunctions.vo theories7/Arith/Max.vo theories7/Reals/Rseries.vo theories7/Reals/SeqProp.vo theories7/Reals/Rcomplete.vo theories7/Reals/PartSum.vo theories7/Reals/AltSeries.vo theories7/Reals/Binomial.vo theories7/Reals/Rsigma.vo theories7/Reals/Rprod.vo theories7/Reals/Cauchy_prod.vo theories7/Reals/Alembert.vo
+theories7/Reals/Rtrigo_fun.vo: theories7/Reals/Rtrigo_fun.v theories7/Reals/Rbase.vo theories7/Reals/Rfunctions.vo theories7/Reals/SeqSeries.vo
+theories7/Reals/Rtrigo_def.vo: theories7/Reals/Rtrigo_def.v theories7/Reals/Rbase.vo theories7/Reals/Rfunctions.vo theories7/Reals/SeqSeries.vo theories7/Reals/Rtrigo_fun.vo theories7/Arith/Max.vo
+theories7/Reals/Rtrigo_alt.vo: theories7/Reals/Rtrigo_alt.v theories7/Reals/Rbase.vo theories7/Reals/Rfunctions.vo theories7/Reals/SeqSeries.vo theories7/Reals/Rtrigo_def.vo
+theories7/Reals/Cos_rel.vo: theories7/Reals/Cos_rel.v theories7/Reals/Rbase.vo theories7/Reals/Rfunctions.vo theories7/Reals/SeqSeries.vo theories7/Reals/Rtrigo_def.vo
+theories7/Reals/Cos_plus.vo: theories7/Reals/Cos_plus.v theories7/Reals/Rbase.vo theories7/Reals/Rfunctions.vo theories7/Reals/SeqSeries.vo theories7/Reals/Rtrigo_def.vo theories7/Reals/Cos_rel.vo theories7/Arith/Max.vo
+theories7/Reals/Rtrigo.vo: theories7/Reals/Rtrigo.v theories7/Reals/Rbase.vo theories7/Reals/Rfunctions.vo theories7/Reals/SeqSeries.vo theories7/Reals/Rtrigo_fun.vo theories7/Reals/Rtrigo_def.vo theories7/Reals/Rtrigo_alt.vo theories7/Reals/Cos_rel.vo theories7/Reals/Cos_plus.vo theories7/ZArith/ZArith_base.vo theories7/ZArith/Zcomplements.vo theories7/Logic/Classical_Prop.vo
+theories7/Reals/Rlimit.vo: theories7/Reals/Rlimit.v theories7/Reals/Rbase.vo theories7/Reals/Rfunctions.vo theories7/Logic/Classical_Prop.vo contrib7/fourier/Fourier.vo
+theories7/Reals/Rderiv.vo: theories7/Reals/Rderiv.v theories7/Reals/Rbase.vo theories7/Reals/Rfunctions.vo theories7/Reals/Rlimit.vo contrib7/fourier/Fourier.vo theories7/Logic/Classical_Prop.vo theories7/Logic/Classical_Pred_Type.vo contrib7/omega/Omega.vo
+theories7/Reals/RList.vo: theories7/Reals/RList.v theories7/Reals/Rbase.vo theories7/Reals/Rfunctions.vo
+theories7/Reals/Ranalysis1.vo: theories7/Reals/Ranalysis1.v theories7/Reals/Rbase.vo theories7/Reals/Rfunctions.vo theories7/Reals/Rlimit.vo theories7/Reals/Rderiv.vo
+theories7/Reals/Ranalysis2.vo: theories7/Reals/Ranalysis2.v theories7/Reals/Rbase.vo theories7/Reals/Rfunctions.vo theories7/Reals/Ranalysis1.vo
+theories7/Reals/Ranalysis3.vo: theories7/Reals/Ranalysis3.v theories7/Reals/Rbase.vo theories7/Reals/Rfunctions.vo theories7/Reals/Ranalysis1.vo theories7/Reals/Ranalysis2.vo
+theories7/Reals/Rtopology.vo: theories7/Reals/Rtopology.v theories7/Reals/Rbase.vo theories7/Reals/Rfunctions.vo theories7/Reals/Ranalysis1.vo theories7/Reals/RList.vo theories7/Logic/Classical_Prop.vo theories7/Logic/Classical_Pred_Type.vo
+theories7/Reals/MVT.vo: theories7/Reals/MVT.v theories7/Reals/Rbase.vo theories7/Reals/Rfunctions.vo theories7/Reals/Ranalysis1.vo theories7/Reals/Rtopology.vo
+theories7/Reals/PSeries_reg.vo: theories7/Reals/PSeries_reg.v theories7/Reals/Rbase.vo theories7/Reals/Rfunctions.vo theories7/Reals/SeqSeries.vo theories7/Reals/Ranalysis1.vo theories7/Arith/Max.vo theories7/Arith/Even.vo
+theories7/Reals/Exp_prop.vo: theories7/Reals/Exp_prop.v theories7/Reals/Rbase.vo theories7/Reals/Rfunctions.vo theories7/Reals/SeqSeries.vo theories7/Reals/Rtrigo.vo theories7/Reals/Ranalysis1.vo theories7/Reals/PSeries_reg.vo theories7/Arith/Div2.vo theories7/Arith/Even.vo theories7/Arith/Max.vo
+theories7/Reals/Rtrigo_reg.vo: theories7/Reals/Rtrigo_reg.v theories7/Reals/Rbase.vo theories7/Reals/Rfunctions.vo theories7/Reals/SeqSeries.vo theories7/Reals/Rtrigo.vo theories7/Reals/Ranalysis1.vo theories7/Reals/PSeries_reg.vo
+theories7/Reals/Rsqrt_def.vo: theories7/Reals/Rsqrt_def.v theories7/Bool/Sumbool.vo theories7/Reals/Rbase.vo theories7/Reals/Rfunctions.vo theories7/Reals/SeqSeries.vo theories7/Reals/Ranalysis1.vo
+theories7/Reals/R_sqrt.vo: theories7/Reals/R_sqrt.v theories7/Reals/Rbase.vo theories7/Reals/Rfunctions.vo theories7/Reals/Rsqrt_def.vo
+theories7/Reals/Rtrigo_calc.vo: theories7/Reals/Rtrigo_calc.v theories7/Reals/Rbase.vo theories7/Reals/Rfunctions.vo theories7/Reals/SeqSeries.vo theories7/Reals/Rtrigo.vo theories7/Reals/R_sqrt.vo
+theories7/Reals/Rgeom.vo: theories7/Reals/Rgeom.v theories7/Reals/Rbase.vo theories7/Reals/Rfunctions.vo theories7/Reals/SeqSeries.vo theories7/Reals/Rtrigo.vo theories7/Reals/R_sqrt.vo
+theories7/Reals/Sqrt_reg.vo: theories7/Reals/Sqrt_reg.v theories7/Reals/Rbase.vo theories7/Reals/Rfunctions.vo theories7/Reals/Ranalysis1.vo theories7/Reals/R_sqrt.vo
+theories7/Reals/Ranalysis4.vo: theories7/Reals/Ranalysis4.v theories7/Reals/Rbase.vo theories7/Reals/Rfunctions.vo theories7/Reals/SeqSeries.vo theories7/Reals/Rtrigo.vo theories7/Reals/Ranalysis1.vo theories7/Reals/Ranalysis3.vo theories7/Reals/Exp_prop.vo
+theories7/Reals/Rpower.vo: theories7/Reals/Rpower.v theories7/Reals/Rbase.vo theories7/Reals/Rfunctions.vo theories7/Reals/SeqSeries.vo theories7/Reals/Rtrigo.vo theories7/Reals/Ranalysis1.vo theories7/Reals/Exp_prop.vo theories7/Reals/Rsqrt_def.vo theories7/Reals/R_sqrt.vo theories7/Reals/MVT.vo theories7/Reals/Ranalysis4.vo
+theories7/Reals/Ranalysis.vo: theories7/Reals/Ranalysis.v theories7/Reals/Rbase.vo theories7/Reals/Rfunctions.vo theories7/Reals/Rtrigo.vo theories7/Reals/SeqSeries.vo theories7/Reals/Ranalysis1.vo theories7/Reals/Ranalysis2.vo theories7/Reals/Ranalysis3.vo theories7/Reals/Rtopology.vo theories7/Reals/MVT.vo theories7/Reals/PSeries_reg.vo theories7/Reals/Exp_prop.vo theories7/Reals/Rtrigo_reg.vo theories7/Reals/Rsqrt_def.vo theories7/Reals/R_sqrt.vo theories7/Reals/Rtrigo_calc.vo theories7/Reals/Rgeom.vo theories7/Reals/RList.vo theories7/Reals/Sqrt_reg.vo theories7/Reals/Ranalysis4.vo theories7/Reals/Rpower.vo
+theories7/Reals/NewtonInt.vo: theories7/Reals/NewtonInt.v theories7/Reals/Rbase.vo theories7/Reals/Rfunctions.vo theories7/Reals/SeqSeries.vo theories7/Reals/Rtrigo.vo theories7/Reals/Ranalysis.vo
+theories7/Reals/RiemannInt_SF.vo: theories7/Reals/RiemannInt_SF.v theories7/Reals/Rbase.vo theories7/Reals/Rfunctions.vo theories7/Reals/Ranalysis.vo theories7/Logic/Classical_Prop.vo
+theories7/Reals/RiemannInt.vo: theories7/Reals/RiemannInt.v theories7/Reals/Rfunctions.vo theories7/Reals/SeqSeries.vo theories7/Reals/Ranalysis.vo theories7/Reals/Rbase.vo theories7/Reals/RiemannInt_SF.vo theories7/Logic/Classical_Prop.vo theories7/Logic/Classical_Pred_Type.vo theories7/Arith/Max.vo
+theories7/Reals/Integration.vo: theories7/Reals/Integration.v theories7/Reals/NewtonInt.vo theories7/Reals/RiemannInt_SF.vo theories7/Reals/RiemannInt.vo
+theories7/Reals/Reals.vo: theories7/Reals/Reals.v theories7/Reals/Rbase.vo theories7/Reals/Rfunctions.vo theories7/Reals/SeqSeries.vo theories7/Reals/Rtrigo.vo theories7/Reals/Ranalysis.vo theories7/Reals/Integration.vo
+theories7/Setoids/Setoid.vo: theories7/Setoids/Setoid.v
+theories7/Sorting/Heap.vo: theories7/Sorting/Heap.v theories7/Lists/PolyList.vo theories7/Sets/Multiset.vo theories7/Sorting/Permutation.vo theories7/Relations/Relations.vo theories7/Sorting/Sorting.vo
+theories7/Sorting/Permutation.vo: theories7/Sorting/Permutation.v theories7/Relations/Relations.vo theories7/Lists/PolyList.vo theories7/Sets/Multiset.vo
+theories7/Sorting/Sorting.vo: theories7/Sorting/Sorting.v theories7/Lists/PolyList.vo theories7/Sets/Multiset.vo theories7/Sorting/Permutation.vo theories7/Relations/Relations.vo
+theories7/Lists/PolyList.vo: theories7/Lists/PolyList.v theories7/Arith/Le.vo
+theories7/Lists/PolyListSyntax.vo: theories7/Lists/PolyListSyntax.v
+theories7/ZArith/Zsyntax.vo: theories7/ZArith/Zsyntax.v theories7/ZArith/BinInt.vo
+theories7/ZArith/zarith_aux.vo: theories7/ZArith/zarith_aux.v theories7/ZArith/BinInt.vo theories7/ZArith/Zcompare.vo theories7/ZArith/Zorder.vo theories7/ZArith/Zmin.vo theories7/ZArith/Zabs.vo
+theories7/ZArith/fast_integer.vo: theories7/ZArith/fast_integer.v theories7/NArith/BinPos.vo theories7/NArith/BinNat.vo theories7/ZArith/BinInt.vo theories7/ZArith/Zcompare.vo theories7/Arith/Mult.vo
+contrib7/omega/OmegaLemmas.vo: contrib7/omega/OmegaLemmas.v theories7/ZArith/ZArith_base.vo
+contrib7/omega/Omega.vo: contrib7/omega/Omega.v theories7/ZArith/ZArith_base.vo contrib7/omega/OmegaLemmas.vo theories7/ZArith/Zhints.vo
+contrib7/romega/ReflOmegaCore.vo: contrib7/romega/ReflOmegaCore.v theories7/Arith/Arith.vo theories7/Lists/PolyList.vo theories7/Bool/Bool.vo theories7/ZArith/ZArith_base.vo contrib7/omega/OmegaLemmas.vo
+contrib7/romega/ROmega.vo: contrib7/romega/ROmega.v contrib7/omega/Omega.vo contrib7/romega/ReflOmegaCore.vo
+contrib7/ring/ArithRing.vo: contrib7/ring/ArithRing.v contrib7/ring/Ring.vo theories7/Arith/Arith.vo theories7/Logic/Eqdep_dec.vo
+contrib7/ring/Ring_normalize.vo: contrib7/ring/Ring_normalize.v contrib7/ring/Ring_theory.vo contrib7/ring/Quote.vo
+contrib7/ring/Ring_theory.vo: contrib7/ring/Ring_theory.v theories7/Bool/Bool.vo
+contrib7/ring/Ring.vo: contrib7/ring/Ring.v theories7/Bool/Bool.vo contrib7/ring/Ring_theory.vo contrib7/ring/Quote.vo contrib7/ring/Ring_normalize.vo contrib7/ring/Ring_abstract.vo
+contrib7/ring/NArithRing.vo: contrib7/ring/NArithRing.v contrib7/ring/Ring.vo theories7/ZArith/ZArith_base.vo theories7/NArith/NArith.vo theories7/Logic/Eqdep_dec.vo
+contrib7/ring/ZArithRing.vo: contrib7/ring/ZArithRing.v contrib7/ring/ArithRing.vo theories7/ZArith/ZArith_base.vo theories7/Logic/Eqdep_dec.vo
+contrib7/ring/Ring_abstract.vo: contrib7/ring/Ring_abstract.v contrib7/ring/Ring_theory.vo contrib7/ring/Quote.vo contrib7/ring/Ring_normalize.vo
+contrib7/ring/Quote.vo: contrib7/ring/Quote.v
+contrib7/ring/Setoid_ring_normalize.vo: contrib7/ring/Setoid_ring_normalize.v contrib7/ring/Setoid_ring_theory.vo contrib7/ring/Quote.vo
+contrib7/ring/Setoid_ring.vo: contrib7/ring/Setoid_ring.v contrib7/ring/Setoid_ring_theory.vo contrib7/ring/Quote.vo contrib7/ring/Setoid_ring_normalize.vo
+contrib7/ring/Setoid_ring_theory.vo: contrib7/ring/Setoid_ring_theory.v theories7/Bool/Bool.vo theories7/Setoids/Setoid.vo
+contrib7/field/Field_Compl.vo: contrib7/field/Field_Compl.v
+contrib7/field/Field_Theory.vo: contrib7/field/Field_Theory.v theories7/Arith/Peano_dec.vo contrib7/ring/Ring.vo contrib7/field/Field_Compl.vo
+contrib7/field/Field_Tactic.vo: contrib7/field/Field_Tactic.v contrib7/ring/Ring.vo contrib7/field/Field_Compl.vo contrib7/field/Field_Theory.vo
+contrib7/field/Field.vo: contrib7/field/Field.v contrib7/field/Field_Compl.vo contrib7/field/Field_Theory.vo contrib7/field/Field_Tactic.vo
+contrib7/correctness/Arrays.vo: contrib7/correctness/Arrays.v contrib7/correctness/ProgInt.vo
+contrib7/correctness/Correctness.vo: contrib7/correctness/Correctness.v contrib7/correctness/Tuples.vo contrib7/correctness/ProgInt.vo contrib7/correctness/ProgBool.vo theories7/ZArith/Zwf.vo contrib7/correctness/Arrays.vo
+contrib7/correctness/Exchange.vo: contrib7/correctness/Exchange.v contrib7/correctness/ProgInt.vo contrib7/correctness/Arrays.vo
+contrib7/correctness/ArrayPermut.vo: contrib7/correctness/ArrayPermut.v contrib7/correctness/ProgInt.vo contrib7/correctness/Arrays.vo contrib7/correctness/Exchange.vo contrib7/omega/Omega.vo
+contrib7/correctness/ProgBool.vo: contrib7/correctness/ProgBool.v theories7/ZArith/ZArith.vo theories7/Arith/Bool_nat.vo theories7/Bool/Sumbool.vo
+contrib7/correctness/ProgInt.vo: contrib7/correctness/ProgInt.v theories7/ZArith/ZArith.vo theories7/ZArith/ZArith_dec.vo
+contrib7/correctness/Sorted.vo: contrib7/correctness/Sorted.v contrib7/correctness/Arrays.vo contrib7/correctness/ArrayPermut.vo contrib7/ring/ZArithRing.vo contrib7/omega/Omega.vo
+contrib7/correctness/Tuples.vo: contrib7/correctness/Tuples.v
+contrib7/fourier/Fourier_util.vo: contrib7/fourier/Fourier_util.v theories7/Reals/Rbase.vo
+contrib7/fourier/Fourier.vo: contrib7/fourier/Fourier.v contrib7/fourier/Fourier_util.vo contrib7/field/Field.vo theories7/Reals/DiscrR.vo
+contrib7/cc/CCSolve.vo: contrib7/cc/CCSolve.v
diff --git a/Makefile b/Makefile
index 8eb8a5653..6e281b73f 100644
--- a/Makefile
+++ b/Makefile
@@ -338,19 +338,21 @@ COQBINARIES= $(COQMKTOP) $(COQC) $(COQTOPBYTE) $(BESTCOQTOP) $(COQTOP) \
 
 coqbinaries:: ${COQBINARIES}
 
-world: coqlib tools coqbinaries coqide
+world: coqlib tools coqbinaries coqide coqlib7
+
+world8: coqlib tools coqbinaries coqide
 
 world7: coqlib7 tools coqbinaries coqide
 
 coqlib:: newtheories newcontrib
 
-coqlib7: theories contrib
+coqlib7: theories7 contrib7
 
 coqlight: theories-light tools coqbinaries
 
-states7:: states/initial.coq
+states7:: states7/initial.coq
 
-states:: states/initial.coq states/initialnew.coq
+states:: states/initial.coq
 
 $(COQTOPOPT): $(COQMKTOP) $(CMX) $(USERTACCMX)
 	$(SHOW)'COQMKTOP -o $@'	
@@ -417,12 +419,12 @@ beforedepend:: ide/utf8_convert.ml
 
 FULLIDELIB=$(FULLCOQLIB)/ide
 
-COQIDEVO=ide/utf8.vo
+OLDCOQIDEVO=ide/utf8.vo
 
-$(COQIDEVO): states/initial.coq
+$(OLDCOQIDEVO): states/initial.coq states7/initial.coq
 	$(BOOTCOQTOP) $(TRANSLATE) -compile $*
 
-IDEFILES=$(COQIDEVO) ide/coq.png ide/.coqide-gtk2rc ide/FAQ
+IDEFILES=$(OLDCOQIDEVO) ide/coq.png ide/.coqide-gtk2rc ide/FAQ
 
 coqide: $(IDEFILES) coqide-$(HASCOQIDE)
 coqide-no:
@@ -432,7 +434,7 @@ coqide-opt:  $(COQIDEBYTE) $(COQIDEOPT) $(COQIDE)
 ide: coqide-$(HASCOQIDE) states
 
 clean-ide: 
-	rm -f ide/utf8.vo $(COQIDECMO) $(COQIDECMX) $(COQIDECMO:.cmo=.cmi) $(COQIDEBYTE) $(COQIDEOPT)
+	rm -f $(OLDCOQIDEVO) $(COQIDECMO) $(COQIDECMX) $(COQIDECMO:.cmo=.cmi) $(COQIDEBYTE) $(COQIDEOPT)
 
 $(COQIDEOPT): $(COQMKTOP) $(CMX) $(USERTACCMX) $(COQIDECMX)
 	$(SHOW)'COQMKTOP -o $@'	
@@ -474,7 +476,7 @@ clean::
 	rm -f ide/extract_index.ml ide/find_phrase.ml ide/highlight.ml
 	rm -f ide/config_lexer.ml ide/config_parser.mli ide/config_parser.ml
 	rm -f ide/utf8_convert.ml
-	rm -f ide/utf8.vo $(COQIDECMO) $(COQIDECMX) $(COQIDECMO:.cmo=.cmi)
+	rm -f $(OLDCOQIDEVO) $(COQIDECMO) $(COQIDECMX) $(COQIDECMO:.cmo=.cmi)
 	rm -f $(COQIDEBYTE) $(COQIDEOPT)
 
 # coqc
@@ -586,12 +588,10 @@ NARITHVO=\
  theories/NArith/BinNat.vo	theories/NArith/NArith.vo
 
 ZARITHVO=\
- theories/ZArith/BinInt.vo \
- theories/ZArith/Wf_Z.vo	theories/ZArith/Zsyntax.vo \
- theories/ZArith/ZArith.vo	theories/ZArith/auxiliary.vo \
- theories/ZArith/ZArith_dec.vo	theories/ZArith/fast_integer.vo \
+ theories/ZArith/BinInt.vo      theories/ZArith/Wf_Z.vo \
+ theories/ZArith/ZArith.vo      theories/ZArith/ZArith_dec.vo \
+ theories/ZArith/auxiliary.vo   theories/ZArith/Zmisc.vo \
  theories/ZArith/Zcompare.vo    theories/ZArith/Znat.vo \
- theories/ZArith/Zmisc.vo	theories/ZArith/zarith_aux.vo \
  theories/ZArith/Zorder.vo      theories/ZArith/Zabs.vo \
  theories/ZArith/Zmin.vo        theories/ZArith/Zeven.vo \
  theories/ZArith/Zhints.vo	theories/ZArith/Zlogarithm.vo \
@@ -602,10 +602,9 @@ ZARITHVO=\
  theories/ZArith/Znumtheory.vo
 
 LISTSVO=\
- theories/Lists/MonoList.vo	theories/Lists/PolyListSyntax.vo \
+ theories/Lists/MonoList.vo \
  theories/Lists/ListSet.vo   	theories/Lists/Streams.vo \
- theories/Lists/PolyList.vo  	theories/Lists/TheoryList.vo \
- theories/Lists/List.vo
+ theories/Lists/TheoryList.vo   theories/Lists/List.vo
 
 SETSVO=\
  theories/Sets/Classical_sets.vo    theories/Sets/Permut.vo \
@@ -686,6 +685,7 @@ REALS_all=\
 REALSVO=$(REALSBASEVO) $(REALS_$(REALS))
 
 ALLREALS=$(REALSBASEVO) $(REALS_all)
+ALLOLDREALS=$(REALSBASEVO:theories%.vo:theories7%.vo) $(REALS_all:theories%.vo:theories7%.vo)
 
 SETOIDSVO=theories/Setoids/Setoid.vo
 
@@ -775,7 +775,7 @@ omega: $(OMEGAVO) $(OMEGACMO) $(ROMEGAVO) $(ROMEGACMO)
 ring: $(RINGVO) $(RINGCMO)
 # xml_ instead of xml to avoid conflict with "make xml"
 xml_: $(XMLVO) $(XMLCMO)
-extraction: $(EXTRACTIONCMO) $(EXTRACTIONVO)
+extraction: $(EXTRACTIONCMO)
 correctness: $(CORRECTNESSCMO) $(CORRECTNESSVO)
 field: $(FIELDVO) $(FIELDCMO)
 fourier: $(FOURIERVO) $(FOURIERCMO)
@@ -783,23 +783,38 @@ jprover: $(JPROVERVO) $(JPROVERCMO)
 funind: $(FUNINDCMO) $(FUNINDVO)
 cc: $(CCVO) $(CCCMO)
 
-NEWINITVO=$(INITVO:%.vo=new%.vo)
-NEWTHEORIESVO=$(THEORIESVO:%.vo=new%.vo)
-NEWCONTRIBVO=$(CONTRIBVO:%.vo=new%.vo)
+NEWINITVO=$(INITVO)
+NEWTHEORIESVO=$(THEORIESVO)
+NEWCONTRIBVO=$(CONTRIBVO)
+
+OBSOLETETHEORIESVO=\
+ theories7/Lists/PolyList.vo theories7/Lists/PolyListSyntax.vo \
+ theories7/ZArith/Zsyntax.vo \
+ theories7/ZArith/zarith_aux.vo	theories7/ZArith/fast_integer.vo
+
+OLDINITVO=$(INITVO:theories%.vo=theories7%.vo)
+OLDTHEORIESVO=$(THEORIESVO:theories%.vo=theories7%.vo) $(OBSOLETETHEORIESVO)
+OLDCONTRIBVO=$(CONTRIBVO:contrib%.vo=contrib7%.vo)
 
-NEWINITV=$(INITVO:%.vo=new%.v)
-NEWTHEORIESV=$(THEORIESVO:%.vo=new%.v)
-NEWCONTRIBV=$(CONTRIBVO:%.vo=new%.v)
+$(CONTRIBVO): states7/initial.coq
+
+NEWINITV=$(INITVO:%.vo=%.v)
+NEWTHEORIESV=$(THEORIESVO:%.vo=%.v)
+NEWCONTRIBV=$(CONTRIBVO:%.vo=%.v)
 
 # Made *.vo and new*.v targets explicit, otherwise "make" 
 # either removes them after use or don't do them (e.g. List.vo)
 newinit:: $(NEWINITV) $(NEWINITVO)
-newtheories:: $(THEORIESVO) $(NEWTHEORIESV) $(NEWTHEORIESVO)
-newcontrib::$(CONTRIBVO) $(NEWCONTRIBV) $(NEWCONTRIBVO) $(CONTRIBCMO)
+newtheories:: $(NEWTHEORIESV) $(NEWTHEORIESVO)
+newcontrib:: $(NEWCONTRIBV) $(NEWCONTRIBVO) $(CONTRIBCMO)
+
+theories7:: $(OLDTHEORIESVO)
+contrib7:: $(OLDCONTRIBVO) 
 
 translation:: $(NEWTHEORIESV) $(NEWCONTRIBV)
 
-ALLVO = $(INITVO) $(THEORIESVO) $(CONTRIBVO) $(EXTRACTIONVO)
+ALLNEWVO = $(INITVO) $(THEORIESVO) $(CONTRIBVO)
+ALLOLDVO = $(OLDINITVO) $(OLDTHEORIESVO) $(OLDCONTRIBVO)
 
 ###########################################################################
 # rules to make theories, contrib and states
@@ -807,78 +822,97 @@ ALLVO = $(INITVO) $(THEORIESVO) $(CONTRIBVO) $(EXTRACTIONVO)
 
 SYNTAXPP=syntax/PPConstr.v syntax/PPCases.v
 
-states/barestate.coq: $(SYNTAXPP) $(BESTCOQTOP)
+states7/barestate.coq: $(SYNTAXPP) $(BESTCOQTOP)
 	$(BESTCOQTOP) -v7 -boot -batch -silent -nois -I syntax -load-vernac-source syntax/MakeBare.v -outputstate $@
 
-states/initial.coq: states/barestate.coq states/MakeInitial.v $(INITVO) $(BESTCOQTOP)
-	$(BOOTCOQTOP) -v7 -batch -silent -is states/barestate.coq -load-vernac-source states/MakeInitial.v -outputstate states/initial.coq
+states7/initial.coq: states7/barestate.coq states7/MakeInitial.v $(OLDINITVO) $(BESTCOQTOP)
+	$(BOOTCOQTOP) -v7 -batch -silent -is states7/barestate.coq -load-vernac-source states7/MakeInitial.v -outputstate states7/initial.coq
 
-states/initialnew.coq: states/MakeInitialNew.v $(NEWINITVO)
-	$(BOOTCOQTOP) -batch -silent -nois -load-vernac-source states/MakeInitialNew.v -outputstate states/initialnew.coq
+states/initial.coq: states/MakeInitial.v $(NEWINITVO)
+	$(BOOTCOQTOP) -batch -silent -nois -load-vernac-source states/MakeInitial.v -outputstate states/initial.coq
 
-newtheories/Init/%.v: $(BESTCOQTOP) theories/Init/%.vo
-	@$(MKDIR) newtheories/Init
-	@cp -f theories/Init/$*.v8  newtheories/Init/$*.v
+#newtheories/Init/%.v: $(BESTCOQTOP) theories/Init/%.vo
+#	@$(MKDIR) newtheories/Init
+#	@cp -f theories/Init/$*.v8  newtheories/Init/$*.v
 
-theories/Init/%.vo: $(BESTCOQTOP) theories/Init/%.v
-	$(BOOTCOQTOP) $(TRANSLATE) -nois -compile theories/Init/$*
+theories7/Init/%.vo: $(BESTCOQTOP) theories7/Init/%.v
+	$(BOOTCOQTOP) $(TRANSLATE) -nois -compile theories7/Init/$*
 
-newtheories/%.v: theories/%.vo
-	@$(MKDIR) newtheories/`dirname $*`
-	@cp -f theories/$*.v8  newtheories/$*.v
+#newtheories/%.v: theories/%.vo
+#	@$(MKDIR) newtheories/`dirname $*`
+#	@cp -f theories/$*.v8  newtheories/$*.v
 
-theories/%.vo: theories/%.v states/initial.coq
-	$(BOOTCOQTOP) $(TRANSLATE) -compile theories/$*
+theories7/%.vo: theories7/%.v states7/initial.coq
+	$(BOOTCOQTOP) $(TRANSLATE) -compile theories7/$*
 
-newcontrib/%.v: contrib/%.vo
-	@$(MKDIR) newcontrib/`dirname $*`
-	@cp -f contrib/$*.v8  newcontrib/$*.v
+#newcontrib/%.v: contrib/%.vo
+#	@$(MKDIR) newcontrib/`dirname $*`
+#	@cp -f contrib/$*.v8  newcontrib/$*.v
 
-contrib/%.vo: contrib/%.v states/initial.coq
-	$(BOOTCOQTOP) $(TRANSLATE) -compile contrib/$*
+contrib7/%.vo: contrib7/%.v states7/initial.coq
+	$(BOOTCOQTOP) $(TRANSLATE) -compile contrib7/$*
 
-newtheories/Init/%.vo: $(BESTCOQTOP) newtheories/Init/%.v
-	$(BOOTCOQTOP) -nois -compile $*
+#newtheories/Init/%.vo: $(BESTCOQTOP) newtheories/Init/%.v
+#	$(BOOTCOQTOP) -nois -compile $*
 
-newtheories/%.vo: newtheories/%.v states/initialnew.coq
-	$(BOOTCOQTOP) -compile newtheories/$*
+theories/Init/%.vo: $(BESTCOQTOP) theories/Init/%.v
+	$(BOOTCOQTOP) -nois -compile theories/Init/$*
 
-newcontrib/%.vo: newcontrib/%.v states/initialnew.coq
-	$(BOOTCOQTOP) -compile newcontrib/$*
+#newtheories/%.vo: newtheories/%.v states/initialnew.coq
+#	$(BOOTCOQTOP) -compile newtheories/$*
+
+theories/%.vo: theories/%.v states/initial.coq
+	$(BOOTCOQTOP) -compile theories/$*
+
+#newcontrib/%.vo: newcontrib/%.v states/initialnew.coq
+#	$(BOOTCOQTOP) -compile newcontrib/$*
+
+contrib/%.vo: contrib/%.v
+	$(BOOTCOQTOP) -compile contrib/$*
 
 contrib/extraction/%.vo: contrib/extraction/%.v states/barestate.coq $(COQC)
-	$(BOOTCOQTOP) $(TRANSLATE) -is states/barestate.coq -compile $*
+	$(BOOTCOQTOP) -is states/barestate.coq -compile $*
+
+contrib7/extraction/%.vo: contrib7/extraction/%.v states/barestate.coq $(COQC)
+	$(BOOTCOQTOP) $(TRANSLATE) -is states7/barestate.coq -compile $*
+
 # Obsolete ?
 contrib/interface/Centaur.vo: contrib/interface/Centaur.v $(INTERFACE)
+	$(BESTCOQTOP) -boot -byte $(COQOPTS) -compile $*
+
+contrib7/interface/Centaur.vo: contrib7/interface/Centaur.v $(INTERFACE)
 	$(BESTCOQTOP) $(TRANSLATE) -boot -byte $(COQOPTS) -compile $*
 
-newtheories/Lists/List.v: newtheories/Lists/PolyList.v
-	(cd newtheories/Lists; cp -f PolyList.v List.v)
+#newtheories/Lists/List.v: newtheories/Lists/PolyList.v
+#	(cd newtheories/Lists; cp -f PolyList.v List.v)
 
-newtheories/Lists/PolyList.vo:
-	@cd #nil command: don't compile it
+#newtheories/Lists/PolyList.vo:
+#	@cd #nil command: don't compile it
 
-newtheories/Lists/PolyListSyntax.vo:
-	@cd #nil command: don't compile it
+#newtheories/Lists/PolyListSyntax.vo:
+#	@cd #nil command: don't compile it
 
-newtheories/ZArith/ZSyntax.vo:
-	@cd #nil command: obsolete, don't compile it
+#newtheories/ZArith/ZSyntax.vo:
+#	@cd #nil command: obsolete, don't compile it
 
-newtheories/ZArith/zarith_aux.vo:
-	@cd #nil command: obsolete, don't compile it
+#newtheories/ZArith/zarith_aux.vo:
+#	@cd #nil command: obsolete, don't compile it
 
 # Obsolete ?
 contrib/interface/AddDad.vo: contrib/interface/AddDad.v $(INTERFACE) states/initial.coq
+	$(BESTCOQTOP) -boot -byte  $(COQOPTS) -compile $*
+
+contrib7/interface/AddDad.vo: contrib7/interface/AddDad.v $(INTERFACE) states7/initial.coq
 	$(BESTCOQTOP) $(TRANSLATE) -boot -byte  $(COQOPTS) -compile $*
 
 clean::
-	rm -f states/*.coq
+	rm -f states/*.coq states7/*.coq
 
 clean::
-	rm -f theories/*/*.vo
+	rm -f theories/*/*.vo theories7/*/*.vo
 
 clean::
-	rm -f contrib/*/*.cm[io] contrib/*/*.vo user-contrib/*.cm[io]
+	rm -f contrib/*/*.cm[io] contrib/*/*.vo contrib7/*/*.vo user-contrib/*.cm[io]
 
 archclean::
 	rm -f contrib/*/*.cmx contrib/*/*.[so]
@@ -1035,6 +1069,8 @@ install-library:
         done
 	$(MKDIR) $(FULLCOQLIB)/states
 	cp states/*.coq $(FULLCOQLIB)/states
+	$(MKDIR) $(FULLCOQLIB)/states7
+	cp states7/*.coq $(FULLCOQLIB)/states7
 	$(MKDIR) $(FULLEMACSLIB)
 	cp tools/coq.el tools/coq-inferior.el $(FULLEMACSLIB)
 	$(MKDIR) $(FULLIDELIB)
@@ -1051,6 +1087,8 @@ install-library-light:
         done
 	$(MKDIR) $(FULLCOQLIB)/states
 	cp states/*.coq $(FULLCOQLIB)/states
+	$(MKDIR) $(FULLCOQLIB)/states7
+	cp states7/*.coq $(FULLCOQLIB)/states7
 	$(MKDIR) $(FULLEMACSLIB)
 	cp tools/coq.el tools/coq-inferior.el $(FULLEMACSLIB)
 
@@ -1366,10 +1404,12 @@ alldepend: depend dependcoq
 
 dependcoq:: beforedepend
 	$(COQDEP) -coqlib . -R theories Coq -R contrib Coq $(COQINCLUDES) \
-	 $(ALLREALS:.vo=.v) $(ALLVO:.vo=.v) > .depend.coq
+	 $(ALLREALS:.vo=.v) $(ALLNEWVO:.vo=.v) > .depend.coq
+	$(COQDEP) -coqlib . -R theories7 Coq -R contrib7 Coq $(COQINCLUDES) \
+	 $(ALLOLDREALS:.vo=.v) $(ALLOLDVO:.vo=.v) > .depend.coq7
 
-.depend.newcoq: .depend.coq Makefile
-	sed -e "s|theories/\([^ ]*\.v\)|newtheories/\1|g" -e "s|contrib/\([^ ]*\.v\)|newcontrib/\1|g" -e "s| newtheories/Lists/PolyListSyntax| newtheories/Lists/List|g" -e "s| newtheories/Lists/PolyList| newtheories/Lists/List|g" .depend.coq > .depend.newcoq
+#.depend.newcoq: .depend.coq Makefile
+#	sed -e "s|theories/\([^ ]*\.v\)|newtheories/\1|g" -e "s|contrib/\([^ ]*\.v\)|newcontrib/\1|g" -e "s| newtheories/Lists/PolyListSyntax| newtheories/Lists/List|g" -e "s| newtheories/Lists/PolyList| newtheories/Lists/List|g" .depend.coq > .depend.newcoq
 
 # Build dependencies ignoring failures in building ml files from ml4 files
 # This is useful to rebuild dependencies when they are strongly corrupted:
@@ -1431,7 +1471,8 @@ devel:
 
 include .depend
 include .depend.coq
-include .depend.newcoq
+#include .depend.newcoq
+include .depend.coq7
 
 clean::
 	rm -fr *.v8 newtheories newcontrib
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index a7de40633..95e29fd21 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -82,9 +82,10 @@ let init_load_path () =
     Mltop.add_path user_contrib Nameops.default_root_prefix;
   (* then standard library *)
   let vdirs = 
-    if !Options.v7 then [ "theories"; "contrib" ]
-    else [ "newtheories"; "newcontrib" ] in
-  let dirs = "states" :: dev @ vdirs @ [ "ide" ] in
+    if !Options.v7 then [ "theories7"; "contrib7" ]
+    else [ "theories"; "contrib" ] in
+  let dirs = 
+    (if !Options.v7 then "states7" else "states") :: dev @ vdirs @ [ "ide" ] in
   List.iter (fun s -> coq_add_rec_path (Filename.concat coqlib s)) dirs;
   let camlp4 = getenv_else "CAMLP4LIB" Coq_config.camlp4lib in
   add_ml_include camlp4;