Renommage en v8 de PolyList en List et List en MonoList

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

7 files changed, 76 insertions, 40 deletions

diff --git a/.depend.coq b/.depend.coq
index fb8ddd00c..e50f67f71 100644
--- a/.depend.coq
+++ b/.depend.coq
@@ -127,12 +127,13 @@ theories/ZArith/Zwf.vo: theories/ZArith/Zwf.v theories/ZArith/ZArith_base.vo the
 theories/ZArith/ZArith_base.vo: theories/ZArith/ZArith_base.v theories/ZArith/fast_integer.vo theories/ZArith/zarith_aux.vo theories/ZArith/auxiliary.vo theories/ZArith/Zsyntax.vo theories/ZArith/ZArith_dec.vo theories/ZArith/Zmisc.vo theories/ZArith/Wf_Z.vo theories/ZArith/Zhints.vo
 theories/ZArith/Zbool.vo: theories/ZArith/Zbool.v theories/ZArith/ZArith_base.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/Lists/List.vo: theories/Lists/List.v theories/Arith/Le.vo
-theories/Lists/PolyListSyntax.vo: theories/Lists/PolyListSyntax.v theories/Lists/PolyList.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/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/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
 theories/Sets/Constructive_sets.vo: theories/Sets/Constructive_sets.v theories/Sets/Ensembles.vo
diff --git a/.depend.newcoq b/.depend.newcoq
index a7299c237..87bfd49f9 100644
--- a/.depend.newcoq
+++ b/.depend.newcoq
@@ -120,19 +120,20 @@ newtheories/ZArith/zarith_aux.vo: newtheories/ZArith/zarith_aux.v newtheories/Ar
 newtheories/ZArith/Zhints.vo: newtheories/ZArith/Zhints.v newtheories/ZArith/zarith_aux.vo newtheories/ZArith/auxiliary.vo newtheories/ZArith/Zsyntax.vo newtheories/ZArith/Zmisc.vo newtheories/ZArith/Wf_Z.vo
 newtheories/ZArith/Zlogarithm.vo: newtheories/ZArith/Zlogarithm.v newtheories/ZArith/ZArith_base.vo newcontrib/omega/Omega.vo newtheories/ZArith/Zcomplements.vo newtheories/ZArith/Zpower.vo
 newtheories/ZArith/Zpower.vo: newtheories/ZArith/Zpower.v newtheories/ZArith/ZArith_base.vo newcontrib/omega/Omega.vo newtheories/ZArith/Zcomplements.vo
-newtheories/ZArith/Zcomplements.vo: newtheories/ZArith/Zcomplements.v newcontrib/ring/ZArithRing.vo newtheories/ZArith/ZArith_base.vo newcontrib/omega/Omega.vo newtheories/Arith/Wf_nat.vo newtheories/Lists/PolyList.vo
+newtheories/ZArith/Zcomplements.vo: newtheories/ZArith/Zcomplements.v newcontrib/ring/ZArithRing.vo newtheories/ZArith/ZArith_base.vo newcontrib/omega/Omega.vo newtheories/Arith/Wf_nat.vo newtheories/Lists/List.vo
 newtheories/ZArith/Zdiv.vo: newtheories/ZArith/Zdiv.v newtheories/ZArith/ZArith_base.vo newcontrib/omega/Omega.vo newcontrib/ring/ZArithRing.vo newtheories/ZArith/Zcomplements.vo
 newtheories/ZArith/Zsqrt.vo: newtheories/ZArith/Zsqrt.v newtheories/ZArith/ZArith_base.vo newcontrib/ring/ZArithRing.vo newcontrib/omega/Omega.vo
 newtheories/ZArith/Zwf.vo: newtheories/ZArith/Zwf.v newtheories/ZArith/ZArith_base.vo newtheories/Arith/Wf_nat.vo newcontrib/omega/Omega.vo
 newtheories/ZArith/ZArith_base.vo: newtheories/ZArith/ZArith_base.v newtheories/ZArith/fast_integer.vo newtheories/ZArith/zarith_aux.vo newtheories/ZArith/auxiliary.vo newtheories/ZArith/Zsyntax.vo newtheories/ZArith/ZArith_dec.vo newtheories/ZArith/Zmisc.vo newtheories/ZArith/Wf_Z.vo newtheories/ZArith/Zhints.vo
 newtheories/ZArith/Zbool.vo: newtheories/ZArith/Zbool.v newtheories/ZArith/ZArith_base.vo newtheories/Bool/Sumbool.vo
 newtheories/ZArith/Zbinary.vo: newtheories/ZArith/Zbinary.v newtheories/Bool/Bvector.vo newtheories/ZArith/ZArith.vo newtheories/ZArith/Zpower.vo newcontrib/omega/Omega.vo
-newtheories/Lists/List.vo: newtheories/Lists/List.v newtheories/Arith/Le.vo
-newtheories/Lists/PolyListSyntax.vo: newtheories/Lists/PolyListSyntax.v newtheories/Lists/PolyList.vo
-newtheories/Lists/ListSet.vo: newtheories/Lists/ListSet.v newtheories/Lists/PolyList.vo
+newtheories/Lists/MonoList.vo: newtheories/Lists/MonoList.v newtheories/Arith/Le.vo
+newtheories/Lists/PolyListSyntax.vo: newtheories/Lists/List.v
+newtheories/Lists/ListSet.vo: newtheories/Lists/ListSet.v newtheories/Lists/List.vo
 newtheories/Lists/Streams.vo: newtheories/Lists/Streams.v
-newtheories/Lists/PolyList.vo: newtheories/Lists/PolyList.v newtheories/Arith/Le.vo
-newtheories/Lists/TheoryList.vo: newtheories/Lists/TheoryList.v newtheories/Lists/PolyList.vo newtheories/Arith/Le.vo newtheories/Arith/Lt.vo newtheories/Arith/Minus.vo newtheories/Bool/DecBool.vo
+newtheories/Lists/PolyList.vo: newtheories/Lists/List.v newtheories/Arith/Le.vo
+newtheories/Lists/TheoryList.vo: newtheories/Lists/TheoryList.v newtheories/Lists/List.vo newtheories/Arith/Le.vo newtheories/Arith/Lt.vo newtheories/Arith/Minus.vo newtheories/Bool/DecBool.vo
+newtheories/Lists/List.vo: newtheories/Lists/List.v newtheories/Arith/Le.vo
 newtheories/Sets/Classical_sets.vo: newtheories/Sets/Classical_sets.v newtheories/Sets/Ensembles.vo newtheories/Sets/Constructive_sets.vo newtheories/Logic/Classical_Type.vo
 newtheories/Sets/Permut.vo: newtheories/Sets/Permut.v
 newtheories/Sets/Constructive_sets.vo: newtheories/Sets/Constructive_sets.v newtheories/Sets/Ensembles.vo
@@ -156,31 +157,31 @@ newtheories/Sets/Relations_3_facts.vo: newtheories/Sets/Relations_3_facts.v newt
 newtheories/Sets/Partial_Order.vo: newtheories/Sets/Partial_Order.v newtheories/Sets/Ensembles.vo newtheories/Sets/Relations_1.vo
 newtheories/Sets/Uniset.vo: newtheories/Sets/Uniset.v newtheories/Bool/Bool.vo newtheories/Sets/Permut.vo
 newtheories/IntMap/Adalloc.vo: newtheories/IntMap/Adalloc.v newtheories/Bool/Bool.vo newtheories/Bool/Sumbool.vo newtheories/ZArith/ZArith.vo newtheories/Arith/Arith.vo newtheories/IntMap/Addr.vo newtheories/IntMap/Adist.vo newtheories/IntMap/Addec.vo newtheories/IntMap/Map.vo newtheories/IntMap/Fset.vo
-newtheories/IntMap/Mapcanon.vo: newtheories/IntMap/Mapcanon.v newtheories/Bool/Bool.vo newtheories/Bool/Sumbool.vo newtheories/Arith/Arith.vo newtheories/ZArith/ZArith.vo newtheories/IntMap/Addr.vo newtheories/IntMap/Adist.vo newtheories/IntMap/Addec.vo newtheories/IntMap/Map.vo newtheories/IntMap/Mapaxioms.vo newtheories/IntMap/Mapiter.vo newtheories/IntMap/Fset.vo newtheories/Lists/PolyList.vo newtheories/IntMap/Lsort.vo newtheories/IntMap/Mapsubset.vo newtheories/IntMap/Mapcard.vo
+newtheories/IntMap/Mapcanon.vo: newtheories/IntMap/Mapcanon.v newtheories/Bool/Bool.vo newtheories/Bool/Sumbool.vo newtheories/Arith/Arith.vo newtheories/ZArith/ZArith.vo newtheories/IntMap/Addr.vo newtheories/IntMap/Adist.vo newtheories/IntMap/Addec.vo newtheories/IntMap/Map.vo newtheories/IntMap/Mapaxioms.vo newtheories/IntMap/Mapiter.vo newtheories/IntMap/Fset.vo newtheories/Lists/List.vo newtheories/IntMap/Lsort.vo newtheories/IntMap/Mapsubset.vo newtheories/IntMap/Mapcard.vo
 newtheories/IntMap/Addec.vo: newtheories/IntMap/Addec.v newtheories/Bool/Bool.vo newtheories/Bool/Sumbool.vo newtheories/ZArith/ZArith.vo newtheories/IntMap/Addr.vo
-newtheories/IntMap/Mapcard.vo: newtheories/IntMap/Mapcard.v newtheories/Bool/Bool.vo newtheories/Bool/Sumbool.vo newtheories/Arith/Arith.vo newtheories/ZArith/ZArith.vo newtheories/IntMap/Addr.vo newtheories/IntMap/Adist.vo newtheories/IntMap/Addec.vo newtheories/IntMap/Map.vo newtheories/IntMap/Mapaxioms.vo newtheories/IntMap/Mapiter.vo newtheories/IntMap/Fset.vo newtheories/IntMap/Mapsubset.vo newtheories/Lists/PolyList.vo newtheories/IntMap/Lsort.vo newtheories/Arith/Peano_dec.vo
+newtheories/IntMap/Mapcard.vo: newtheories/IntMap/Mapcard.v newtheories/Bool/Bool.vo newtheories/Bool/Sumbool.vo newtheories/Arith/Arith.vo newtheories/ZArith/ZArith.vo newtheories/IntMap/Addr.vo newtheories/IntMap/Adist.vo newtheories/IntMap/Addec.vo newtheories/IntMap/Map.vo newtheories/IntMap/Mapaxioms.vo newtheories/IntMap/Mapiter.vo newtheories/IntMap/Fset.vo newtheories/IntMap/Mapsubset.vo newtheories/Lists/List.vo newtheories/IntMap/Lsort.vo newtheories/Arith/Peano_dec.vo
 newtheories/IntMap/Addr.vo: newtheories/IntMap/Addr.v newtheories/Bool/Bool.vo newtheories/ZArith/ZArith.vo
-newtheories/IntMap/Mapc.vo: newtheories/IntMap/Mapc.v newtheories/Bool/Bool.vo newtheories/Bool/Sumbool.vo newtheories/Arith/Arith.vo newtheories/ZArith/ZArith.vo newtheories/IntMap/Addr.vo newtheories/IntMap/Adist.vo newtheories/IntMap/Addec.vo newtheories/IntMap/Map.vo newtheories/IntMap/Mapaxioms.vo newtheories/IntMap/Fset.vo newtheories/IntMap/Mapiter.vo newtheories/IntMap/Mapsubset.vo newtheories/Lists/PolyList.vo newtheories/IntMap/Lsort.vo newtheories/IntMap/Mapcard.vo newtheories/IntMap/Mapcanon.vo
+newtheories/IntMap/Mapc.vo: newtheories/IntMap/Mapc.v newtheories/Bool/Bool.vo newtheories/Bool/Sumbool.vo newtheories/Arith/Arith.vo newtheories/ZArith/ZArith.vo newtheories/IntMap/Addr.vo newtheories/IntMap/Adist.vo newtheories/IntMap/Addec.vo newtheories/IntMap/Map.vo newtheories/IntMap/Mapaxioms.vo newtheories/IntMap/Fset.vo newtheories/IntMap/Mapiter.vo newtheories/IntMap/Mapsubset.vo newtheories/Lists/List.vo newtheories/IntMap/Lsort.vo newtheories/IntMap/Mapcard.vo newtheories/IntMap/Mapcanon.vo
 newtheories/IntMap/Adist.vo: newtheories/IntMap/Adist.v newtheories/Bool/Bool.vo newtheories/ZArith/ZArith.vo newtheories/Arith/Arith.vo newtheories/Arith/Min.vo newtheories/IntMap/Addr.vo
-newtheories/IntMap/Mapfold.vo: newtheories/IntMap/Mapfold.v newtheories/Bool/Bool.vo newtheories/Bool/Sumbool.vo newtheories/ZArith/ZArith.vo newtheories/IntMap/Addr.vo newtheories/IntMap/Adist.vo newtheories/IntMap/Addec.vo newtheories/IntMap/Map.vo newtheories/IntMap/Fset.vo newtheories/IntMap/Mapaxioms.vo newtheories/IntMap/Mapiter.vo newtheories/IntMap/Lsort.vo newtheories/IntMap/Mapsubset.vo newtheories/Lists/PolyList.vo
+newtheories/IntMap/Mapfold.vo: newtheories/IntMap/Mapfold.v newtheories/Bool/Bool.vo newtheories/Bool/Sumbool.vo newtheories/ZArith/ZArith.vo newtheories/IntMap/Addr.vo newtheories/IntMap/Adist.vo newtheories/IntMap/Addec.vo newtheories/IntMap/Map.vo newtheories/IntMap/Fset.vo newtheories/IntMap/Mapaxioms.vo newtheories/IntMap/Mapiter.vo newtheories/IntMap/Lsort.vo newtheories/IntMap/Mapsubset.vo newtheories/Lists/List.vo
 newtheories/IntMap/Allmaps.vo: newtheories/IntMap/Allmaps.v newtheories/IntMap/Addr.vo newtheories/IntMap/Adist.vo newtheories/IntMap/Addec.vo newtheories/IntMap/Map.vo newtheories/IntMap/Fset.vo newtheories/IntMap/Mapaxioms.vo newtheories/IntMap/Mapiter.vo newtheories/IntMap/Mapsubset.vo newtheories/IntMap/Lsort.vo newtheories/IntMap/Mapfold.vo newtheories/IntMap/Mapcard.vo newtheories/IntMap/Mapcanon.vo newtheories/IntMap/Mapc.vo newtheories/IntMap/Maplists.vo newtheories/IntMap/Adalloc.vo
-newtheories/IntMap/Mapiter.vo: newtheories/IntMap/Mapiter.v newtheories/Bool/Bool.vo newtheories/Bool/Sumbool.vo newtheories/ZArith/ZArith.vo newtheories/IntMap/Addr.vo newtheories/IntMap/Adist.vo newtheories/IntMap/Addec.vo newtheories/IntMap/Map.vo newtheories/IntMap/Mapaxioms.vo newtheories/IntMap/Fset.vo newtheories/Lists/PolyList.vo
+newtheories/IntMap/Mapiter.vo: newtheories/IntMap/Mapiter.v newtheories/Bool/Bool.vo newtheories/Bool/Sumbool.vo newtheories/ZArith/ZArith.vo newtheories/IntMap/Addr.vo newtheories/IntMap/Adist.vo newtheories/IntMap/Addec.vo newtheories/IntMap/Map.vo newtheories/IntMap/Mapaxioms.vo newtheories/IntMap/Fset.vo newtheories/Lists/List.vo
 newtheories/IntMap/Fset.vo: newtheories/IntMap/Fset.v newtheories/Bool/Bool.vo newtheories/Bool/Sumbool.vo newtheories/ZArith/ZArith.vo newtheories/IntMap/Addr.vo newtheories/IntMap/Adist.vo newtheories/IntMap/Addec.vo newtheories/IntMap/Map.vo
-newtheories/IntMap/Maplists.vo: newtheories/IntMap/Maplists.v newtheories/IntMap/Addr.vo newtheories/IntMap/Addec.vo newtheories/IntMap/Map.vo newtheories/IntMap/Fset.vo newtheories/IntMap/Mapaxioms.vo newtheories/IntMap/Mapsubset.vo newtheories/IntMap/Mapcard.vo newtheories/IntMap/Mapcanon.vo newtheories/IntMap/Mapc.vo newtheories/Bool/Bool.vo newtheories/Bool/Sumbool.vo newtheories/Lists/PolyList.vo newtheories/Arith/Arith.vo newtheories/IntMap/Mapiter.vo newtheories/IntMap/Mapfold.vo
-newtheories/IntMap/Lsort.vo: newtheories/IntMap/Lsort.v newtheories/Bool/Bool.vo newtheories/Bool/Sumbool.vo newtheories/Arith/Arith.vo newtheories/ZArith/ZArith.vo newtheories/IntMap/Addr.vo newtheories/IntMap/Adist.vo newtheories/IntMap/Addec.vo newtheories/IntMap/Map.vo newtheories/Lists/PolyList.vo newtheories/IntMap/Mapiter.vo
+newtheories/IntMap/Maplists.vo: newtheories/IntMap/Maplists.v newtheories/IntMap/Addr.vo newtheories/IntMap/Addec.vo newtheories/IntMap/Map.vo newtheories/IntMap/Fset.vo newtheories/IntMap/Mapaxioms.vo newtheories/IntMap/Mapsubset.vo newtheories/IntMap/Mapcard.vo newtheories/IntMap/Mapcanon.vo newtheories/IntMap/Mapc.vo newtheories/Bool/Bool.vo newtheories/Bool/Sumbool.vo newtheories/Lists/List.vo newtheories/Arith/Arith.vo newtheories/IntMap/Mapiter.vo newtheories/IntMap/Mapfold.vo
+newtheories/IntMap/Lsort.vo: newtheories/IntMap/Lsort.v newtheories/Bool/Bool.vo newtheories/Bool/Sumbool.vo newtheories/Arith/Arith.vo newtheories/ZArith/ZArith.vo newtheories/IntMap/Addr.vo newtheories/IntMap/Adist.vo newtheories/IntMap/Addec.vo newtheories/IntMap/Map.vo newtheories/Lists/List.vo newtheories/IntMap/Mapiter.vo
 newtheories/IntMap/Mapsubset.vo: newtheories/IntMap/Mapsubset.v newtheories/Bool/Bool.vo newtheories/Bool/Sumbool.vo newtheories/Arith/Arith.vo newtheories/ZArith/ZArith.vo newtheories/IntMap/Addr.vo newtheories/IntMap/Adist.vo newtheories/IntMap/Addec.vo newtheories/IntMap/Map.vo newtheories/IntMap/Fset.vo newtheories/IntMap/Mapaxioms.vo newtheories/IntMap/Mapiter.vo
 newtheories/IntMap/Mapaxioms.vo: newtheories/IntMap/Mapaxioms.v newtheories/Bool/Bool.vo newtheories/Bool/Sumbool.vo newtheories/ZArith/ZArith.vo newtheories/IntMap/Addr.vo newtheories/IntMap/Adist.vo newtheories/IntMap/Addec.vo newtheories/IntMap/Map.vo newtheories/IntMap/Fset.vo
 newtheories/IntMap/Map.vo: newtheories/IntMap/Map.v newtheories/Bool/Bool.vo newtheories/Bool/Sumbool.vo newtheories/ZArith/ZArith.vo newtheories/IntMap/Addr.vo newtheories/IntMap/Adist.vo newtheories/IntMap/Addec.vo
 newtheories/Relations/Newman.vo: newtheories/Relations/Newman.v newtheories/Relations/Rstar.vo
 newtheories/Relations/Operators_Properties.vo: newtheories/Relations/Operators_Properties.v newtheories/Relations/Relation_Definitions.vo newtheories/Relations/Relation_Operators.vo
 newtheories/Relations/Relation_Definitions.vo: newtheories/Relations/Relation_Definitions.v
-newtheories/Relations/Relation_Operators.vo: newtheories/Relations/Relation_Operators.v newtheories/Relations/Relation_Definitions.vo newtheories/Lists/PolyList.vo newtheories/Lists/PolyListSyntax.vo
+newtheories/Relations/Relation_Operators.vo: newtheories/Relations/Relation_Operators.v newtheories/Relations/Relation_Definitions.vo newtheories/Lists/List.vo newtheories/Lists/List.vo
 newtheories/Relations/Relations.vo: newtheories/Relations/Relations.v newtheories/Relations/Relation_Definitions.vo newtheories/Relations/Relation_Operators.vo newtheories/Relations/Operators_Properties.vo
 newtheories/Relations/Rstar.vo: newtheories/Relations/Rstar.v
 newtheories/Wellfounded/Disjoint_Union.vo: newtheories/Wellfounded/Disjoint_Union.v newtheories/Relations/Relation_Operators.vo
 newtheories/Wellfounded/Inclusion.vo: newtheories/Wellfounded/Inclusion.v newtheories/Relations/Relation_Definitions.vo
 newtheories/Wellfounded/Inverse_Image.vo: newtheories/Wellfounded/Inverse_Image.v
-newtheories/Wellfounded/Lexicographic_Exponentiation.vo: newtheories/Wellfounded/Lexicographic_Exponentiation.v newtheories/Logic/Eqdep.vo newtheories/Lists/PolyList.vo newtheories/Lists/PolyListSyntax.vo newtheories/Relations/Relation_Operators.vo newtheories/Wellfounded/Transitive_Closure.vo
+newtheories/Wellfounded/Lexicographic_Exponentiation.vo: newtheories/Wellfounded/Lexicographic_Exponentiation.v newtheories/Logic/Eqdep.vo newtheories/Lists/List.vo newtheories/Lists/List.vo newtheories/Relations/Relation_Operators.vo newtheories/Wellfounded/Transitive_Closure.vo
 newtheories/Wellfounded/Transitive_Closure.vo: newtheories/Wellfounded/Transitive_Closure.v newtheories/Relations/Relation_Definitions.vo newtheories/Relations/Relation_Operators.vo
 newtheories/Wellfounded/Union.vo: newtheories/Wellfounded/Union.v newtheories/Relations/Relation_Operators.vo newtheories/Relations/Relation_Definitions.vo newtheories/Wellfounded/Transitive_Closure.vo
 newtheories/Wellfounded/Wellfounded.vo: newtheories/Wellfounded/Wellfounded.v newtheories/Wellfounded/Disjoint_Union.vo newtheories/Wellfounded/Inclusion.vo newtheories/Wellfounded/Inverse_Image.vo newtheories/Wellfounded/Lexicographic_Exponentiation.vo newtheories/Wellfounded/Lexicographic_Product.vo newtheories/Wellfounded/Transitive_Closure.vo newtheories/Wellfounded/Union.vo newtheories/Wellfounded/Well_Ordering.vo
@@ -241,11 +242,11 @@ newtheories/Reals/RiemannInt.vo: newtheories/Reals/RiemannInt.v newtheories/Real
 newtheories/Reals/Integration.vo: newtheories/Reals/Integration.v newtheories/Reals/NewtonInt.vo newtheories/Reals/RiemannInt_SF.vo newtheories/Reals/RiemannInt.vo
 newtheories/Reals/Reals.vo: newtheories/Reals/Reals.v newtheories/Reals/Rbase.vo newtheories/Reals/Rfunctions.vo newtheories/Reals/SeqSeries.vo newtheories/Reals/Rtrigo.vo newtheories/Reals/Ranalysis.vo newtheories/Reals/Integration.vo
 newtheories/Setoids/Setoid.vo: newtheories/Setoids/Setoid.v
-newtheories/Sorting/Heap.vo: newtheories/Sorting/Heap.v newtheories/Lists/PolyList.vo newtheories/Sets/Multiset.vo newtheories/Sorting/Permutation.vo newtheories/Relations/Relations.vo newtheories/Sorting/Sorting.vo
-newtheories/Sorting/Permutation.vo: newtheories/Sorting/Permutation.v newtheories/Relations/Relations.vo newtheories/Lists/PolyList.vo newtheories/Sets/Multiset.vo
-newtheories/Sorting/Sorting.vo: newtheories/Sorting/Sorting.v newtheories/Lists/PolyList.vo newtheories/Sets/Multiset.vo newtheories/Sorting/Permutation.vo newtheories/Relations/Relations.vo
+newtheories/Sorting/Heap.vo: newtheories/Sorting/Heap.v newtheories/Lists/List.vo newtheories/Sets/Multiset.vo newtheories/Sorting/Permutation.vo newtheories/Relations/Relations.vo newtheories/Sorting/Sorting.vo
+newtheories/Sorting/Permutation.vo: newtheories/Sorting/Permutation.v newtheories/Relations/Relations.vo newtheories/Lists/List.vo newtheories/Sets/Multiset.vo
+newtheories/Sorting/Sorting.vo: newtheories/Sorting/Sorting.v newtheories/Lists/List.vo newtheories/Sets/Multiset.vo newtheories/Sorting/Permutation.vo newtheories/Relations/Relations.vo
 newcontrib/omega/Omega.vo: newcontrib/omega/Omega.v newtheories/ZArith/fast_integer.vo newtheories/ZArith/zarith_aux.vo newtheories/ZArith/auxiliary.vo newtheories/ZArith/Zsyntax.vo newtheories/ZArith/ZArith_dec.vo newtheories/ZArith/Zmisc.vo newtheories/ZArith/Wf_Z.vo newtheories/ZArith/Zhints.vo
-newcontrib/romega/ReflOmegaCore.vo: newcontrib/romega/ReflOmegaCore.v newtheories/Arith/Arith.vo newtheories/Lists/PolyList.vo newtheories/Bool/Bool.vo newtheories/ZArith/ZArith_base.vo
+newcontrib/romega/ReflOmegaCore.vo: newcontrib/romega/ReflOmegaCore.v newtheories/Arith/Arith.vo newtheories/Lists/List.vo newtheories/Bool/Bool.vo newtheories/ZArith/ZArith_base.vo
 newcontrib/romega/ROmega.vo: newcontrib/romega/ROmega.v newcontrib/omega/Omega.vo newcontrib/romega/ReflOmegaCore.vo
 newcontrib/ring/ArithRing.vo: newcontrib/ring/ArithRing.v newcontrib/ring/Ring.vo newtheories/Arith/Arith.vo newtheories/Logic/Eqdep_dec.vo
 newcontrib/ring/Ring_normalize.vo: newcontrib/ring/Ring_normalize.v newcontrib/ring/Ring_theory.vo newcontrib/ring/Quote.vo
diff --git a/Makefile b/Makefile
index de7b0c104..c8ceec78c 100644
--- a/Makefile
+++ b/Makefile
@@ -579,9 +579,10 @@ ZARITHVO=\
  theories/ZArith/Zbool.vo	theories/ZArith/Zbinary.vo
 
 LISTSVO=\
- theories/Lists/List.vo		theories/Lists/PolyListSyntax.vo \
+ theories/Lists/MonoList.vo	theories/Lists/PolyListSyntax.vo \
  theories/Lists/ListSet.vo   	theories/Lists/Streams.vo \
- theories/Lists/PolyList.vo  	theories/Lists/TheoryList.vo
+ theories/Lists/PolyList.vo  	theories/Lists/TheoryList.vo \
+ theories/Lists/List.vo
 
 SETSVO=\
  theories/Sets/Classical_sets.vo    theories/Sets/Permut.vo \
@@ -678,7 +679,7 @@ logic: $(LOGICVO:%.vo=new%.vo)
 arith: $(ARITHVO:%.vo=new%.vo)
 bool: $(BOOLVO:%.vo=new%.vo)
 zarith: $(ZARITHVO:%.vo=new%.vo)
-lists: $(LISTSVO:%.vo=new%.vo)
+lists: $(LISTVO) $(LISTSVO:%.vo=new%.vo)
 sets: $(SETSVO:%.vo=new%.vo)
 intmap: $(INTMAPVO:%.vo=new%.vo)
 relations: $(RELATIONSVO:%.vo=new%.vo)
@@ -765,10 +766,11 @@ NEWINITV=$(INITVO:%.vo=new%.v)
 NEWTHEORIESV=$(THEORIESVO:%.vo=new%.v)
 NEWCONTRIBV=$(CONTRIBVO:%.vo=new%.v)
 
-# Made new*.v targets explicit, otherwise "make" removes them after use
+# 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:: $(NEWTHEORIESV) $(NEWTHEORIESVO)
-newcontrib:: $(NEWCONTRIBV) $(NEWCONTRIBVO) $(CONTRIBCMO)
+newtheories:: $(THEORIESVO) $(NEWTHEORIESV) $(NEWTHEORIESVO)
+newcontrib::$(CONTRIBVO) $(NEWCONTRIBV) $(NEWCONTRIBVO) $(CONTRIBCMO)
 
 translation:: $(NEWTHEORIESV) $(NEWCONTRIBV)
 
@@ -825,6 +827,15 @@ contrib/extraction/%.vo: contrib/extraction/%.v states/barestate.coq $(COQC)
 contrib/interface/Centaur.vo: contrib/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/PolyList.vo:
+	rm newtheories/Lists/PolyList.v
+
+newtheories/Lists/PolyListSyntax.vo:
+	rm newtheories/Lists/PolyListSyntax.v
+
 # Obsolete ?
 contrib/interface/AddDad.vo: contrib/interface/AddDad.v $(INTERFACE) states/initial.coq
 	$(BESTCOQTOP) $(TRANSLATE) -boot -byte  $(COQOPTS) -compile $*
@@ -977,6 +988,8 @@ NEWLIBFILES=$(NEWTHEORIESVO) $(NEWCONTRIBVO)
 NEWLIBFILESLIGHT=$(NEWTHEORIESLIGHTVO)
 
 install-library:
+	- rm newtheories/Lists/PolyList.v{,o}        #obsolete module
+	- rm newtheories/Lists/PolyListSyntax.v{,o}  #obsolete module
 	$(MKDIR) $(FULLCOQLIB)
 	for f in $(LIBFILES) $(NEWLIBFILES); do \
 	  $(MKDIR) $(FULLCOQLIB)/`dirname $$f`; \
@@ -1296,7 +1309,7 @@ dependcoq:: beforedepend
 	 $(ALLREALS:.vo=.v) $(ALLVO:.vo=.v) > .depend.coq
 
 .depend.newcoq: .depend.coq Makefile
-	sed -e "s|theories/\([^ ]*\.v\)|newtheories/\1|g" -e "s|contrib/\([^ ]*\.v\)|newcontrib/\1|g" .depend.coq > .depend.newcoq
+	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:
diff --git a/theories/Lists/PolyList.v b/theories/Lists/PolyList.v
index 681e0cb1c..450fedfc6 100644
--- a/theories/Lists/PolyList.v
+++ b/theories/Lists/PolyList.v
@@ -631,3 +631,11 @@ Reflexivity.
 Qed.
 
 End Functions_on_lists.
+
+(** Exporting list notations *)
+
+V8Infix "::" cons (at level 45, right associativity) : list_scope.
+
+Infix RIGHTA 7 "^" app : list_scope V8only RIGHTA 45 "++".
+
+Open Scope list_scope.
diff --git a/theories/Lists/PolyListSyntax.v b/theories/Lists/PolyListSyntax.v
index 640cf3fbf..a4b6a57aa 100644
--- a/theories/Lists/PolyListSyntax.v
+++ b/theories/Lists/PolyListSyntax.v
@@ -8,12 +8,3 @@
 
 (*i $Id$ i*)
 
-(** Syntax for list concatenation *)
-
-Require PolyList.
-
-V8Infix "::" cons (at level 45, right associativity) : list_scope.
-
-Infix RIGHTA 7 "^" app : list_scope V8only RIGHTA 45 "++".
-
-Open Scope list_scope.
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 6665af74c..af4a705b4 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -508,11 +508,20 @@ let is_obsolete_module (_,qid) =
 	  | "EqDecide" | "Xml" |  "Extraction" | "Tauto" | "Setoid_replace"
           | "Elimdep" 
 	  | "DatatypesSyntax" | "LogicSyntax" | "Logic_TypeSyntax"
-	  | "SpecifSyntax" | "PeanoSyntax" | "TypeSyntax")
+	  | "SpecifSyntax" | "PeanoSyntax" | "TypeSyntax" | "PolyListSyntax")
 	  -> true
 	| _ -> false)
   | _ -> false
 
+let test_renamed_module (_,qid) =
+  match repr_qualid qid with
+  | dir, id when dir = empty_dirpath ->
+      (match string_of_id id with
+	| "List" -> warning "List has been renamed into MonoList"
+        | "PolyList" -> warning "PolyList has been renamed into List and old List into MonoList"
+        | _ -> ())
+  | _ -> ()
+
 let vernac_require import _ qidl =
   let qidl = List.map qualid_of_reference qidl in
   try
@@ -528,6 +537,7 @@ let vernac_require import _ qidl =
 	  warning ("Module "^(string_of_qualid qid)^
 	  " is now built-in and shouldn't be required")) qidl
     else
+      if not !Options.v7 then List.iter test_renamed_module qidl;
       raise e
       
 let vernac_import export refl =
diff --git a/translate/ppvernacnew.ml b/translate/ppvernacnew.ml
index b04ff3efc..1e392b548 100644
--- a/translate/ppvernacnew.ml
+++ b/translate/ppvernacnew.ml
@@ -33,7 +33,19 @@ let pr_id id = pr_id (Constrextern.v7_to_v8_id id)
 
 let pr_ltac_id id = pr_id (id_of_ltac_v7_id id)
 
-let pr_module = Libnames.pr_reference
+let pr_module r =
+  let update_ref s = match r with
+    | Ident (loc,_) ->
+        Ident (loc,id_of_string s)
+    | Qualid (loc,qid) ->
+        Qualid (loc,make_qualid (fst (repr_qualid qid)) (id_of_string s)) in
+  let (_,dir,_) =
+    Library.locate_qualified_library (snd (qualid_of_reference r)) in
+  let r = match List.rev (List.map string_of_id (repr_dirpath dir)) with
+    | [ "Coq"; "Lists"; "List" ] -> update_ref "MonoList"
+    | [ "Coq"; "Lists"; "PolyList" ] -> update_ref "List"
+    | _ -> r in
+  Libnames.pr_reference r
 
 let pr_reference r =
   let loc = loc_of_reference r in
@@ -1097,7 +1109,7 @@ let pr_vernac = function
 	["Refine"; "Inv"; "Equality"; "EAuto"; "AutoRewrite"; "EqDecide"; 
          "Xml"; "Extraction"; "Tauto"; "Setoid_replace";"Elimdep";
 	 "DatatypesSyntax"; "LogicSyntax"; "Logic_TypeSyntax";
-	 "SpecifSyntax"; "PeanoSyntax"; "TypeSyntax"] ->
+	 "SpecifSyntax"; "PeanoSyntax"; "TypeSyntax"; "PolyListSyntax"] ->
       warning ("Forgetting obsolete module "^(string_of_id r));
       mt()
   | VernacSyntax _  | VernacGrammar _ as x -> pr_vernac x