list, length, app are migrated from List to Datatypes

This allows easier handling of dependencies, for instance RelationClasses
won't have to requires List (which itself requires part of Arith, etc).
One of the underlying ideas is to provide setoid rewriting in Init someday.

Thanks to some notations in List, this change should be fairly transparent
to the user. For instance, one could see that List.length is a notation for
(Datatypes.)length only when doing a Print List.length.

For these notations not to be too intrusive, they are hidden behind an explicit
Export of Datatypes at the end of List. This isn't very pretty, but quite handy.
Notation.ml is patched to stop complaining in the case of reloading the same
Delimit Scope twice.

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

1 files changed, 1 insertions, 1 deletions

diff --git a/theories/Relations/Relation_Operators.v b/theories/Relations/Relation_Operators.v
index 8fea0abc4..39e0331d5 100644
--- a/theories/Relations/Relation_Operators.v
+++ b/theories/Relations/Relation_Operators.v
@@ -17,7 +17,6 @@
 (************************************************************************)
 
 Require Import Relation_Definitions.
-Require Import List.
 
 (** * Some operators to build relations *)
 
@@ -187,6 +186,7 @@ Section Swap.
     | sp_swap x y (p:A * A) : symprod A A R R (x, y) p -> swapprod (y, x) p.
 End Swap.
 
+Local Open Scope list_scope.
 
 Section Lexicographic_Exponentiation.