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

5 files changed, 79 insertions, 71 deletions

diff --git a/interp/notation.ml b/interp/notation.ml
index 6ae720fca..39ae27823 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -147,18 +147,23 @@ let delimiters_map = ref Gmap.empty
 
 let declare_delimiters scope key =
   let sc = find_scope scope in
-  if sc.delimiters <> None && Flags.is_verbose () then begin
-    let old = Option.get sc.delimiters in
-    Flags.if_verbose
-      warning ("Overwritting previous delimiting key "^old^" in scope "^scope)
+  let newsc = { sc with delimiters = Some key } in
+  begin match sc.delimiters with
+    | None -> scope_map := Gmap.add scope newsc !scope_map
+    | Some oldkey when oldkey = key -> ()
+    | Some oldkey ->
+	Flags.if_verbose warning
+	  ("Overwritting previous delimiting key "^oldkey^" in scope "^scope);
+	scope_map := Gmap.add scope newsc !scope_map
   end;
-  let sc = { sc with delimiters = Some key } in
-  scope_map := Gmap.add scope sc !scope_map;
-  if Gmap.mem key !delimiters_map then begin
-    let oldsc = Gmap.find key !delimiters_map in
-    Flags.if_verbose warning ("Hiding binding of key "^key^" to "^oldsc)
-  end;
-  delimiters_map := Gmap.add key scope !delimiters_map
+  try
+    let oldscope = Gmap.find key !delimiters_map in
+    if oldscope = scope then ()
+    else begin
+      Flags.if_verbose warning ("Hiding binding of key "^key^" to "^oldscope);
+      delimiters_map := Gmap.add key scope !delimiters_map
+    end
+  with Not_found -> delimiters_map := Gmap.add key scope !delimiters_map
 
 let find_delimiters_scope loc key =
   try Gmap.find key !delimiters_map
diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v
index cc3cae4da..06da51129 100644
--- a/theories/Classes/RelationClasses.v
+++ b/theories/Classes/RelationClasses.v
@@ -203,13 +203,11 @@ Program Instance iff_equivalence : Equivalence iff.
    The resulting theory can be applied to homogeneous binary relations but also to
    arbitrary n-ary predicates. *)
 
-Require Import Coq.Lists.List.
+Local Open Scope list_scope.
 
 (* Notation " [ ] " := nil : list_scope. *)
 (* Notation " [ x ; .. ; y ] " := (cons x .. (cons y nil) ..) (at level 1) : list_scope. *)
 
-(* Open Local Scope list_scope. *)
-
 (** A compact representation of non-dependent arities, with the codomain singled-out. *)
 
 Fixpoint arrows (l : list Type) (r : Type) : Type :=
@@ -220,9 +218,9 @@ Fixpoint arrows (l : list Type) (r : Type) : Type :=
 
 (** We can define abbreviations for operation and relation types based on [arrows]. *)
 
-Definition unary_operation A := arrows (cons A nil) A.
-Definition binary_operation A := arrows (cons A (cons A nil)) A.
-Definition ternary_operation A := arrows (cons A (cons A (cons A nil))) A.
+Definition unary_operation A := arrows (A::nil) A.
+Definition binary_operation A := arrows (A::A::nil) A.
+Definition ternary_operation A := arrows (A::A::A::nil) A.
 
 (** We define n-ary [predicate]s as functions into [Prop]. *)
 
@@ -230,11 +228,11 @@ Notation predicate l := (arrows l Prop).
 
 (** Unary predicates, or sets. *)
 
-Definition unary_predicate A := predicate (cons A nil).
+Definition unary_predicate A := predicate (A::nil).
 
 (** Homogeneous binary relations, equivalent to [relation A]. *)
 
-Definition binary_relation A := predicate (cons A (cons A nil)).
+Definition binary_relation A := predicate (A::A::nil).
 
 (** We can close a predicate by universal or existential quantification. *)
 
@@ -345,18 +343,18 @@ Program Instance predicate_implication_preorder :
    from the general ones. *)
 
 Definition relation_equivalence {A : Type} : relation (relation A) :=
-  @predicate_equivalence (cons _ (cons _ nil)).
+  @predicate_equivalence (_::_::nil).
 
 Class subrelation {A:Type} (R R' : relation A) : Prop :=
-  is_subrelation : @predicate_implication (cons A (cons A nil)) R R'.
+  is_subrelation : @predicate_implication (A::A::nil) R R'.
 
 Implicit Arguments subrelation [[A]].
 
 Definition relation_conjunction {A} (R : relation A) (R' : relation A) : relation A :=
-  @predicate_intersection (cons A (cons A nil)) R R'.
+  @predicate_intersection (A::A::nil) R R'.
 
 Definition relation_disjunction {A} (R : relation A) (R' : relation A) : relation A :=
-  @predicate_union (cons A (cons A nil)) R R'.
+  @predicate_union (A::A::nil) R R'.
 
 (** Relation equivalence is an equivalence, and subrelation defines a partial order. *)
 
@@ -364,10 +362,10 @@ Set Automatic Introduction.
 
 Instance relation_equivalence_equivalence (A : Type) :
   Equivalence (@relation_equivalence A).
-Proof. exact (@predicate_equivalence_equivalence (cons A (cons A nil))). Qed.
+Proof. exact (@predicate_equivalence_equivalence (A::A::nil)). Qed.
 
 Instance relation_implication_preorder A : PreOrder (@subrelation A).
-Proof. exact (@predicate_implication_preorder (cons A (cons A nil))). Qed.
+Proof. exact (@predicate_implication_preorder (A::A::nil)). Qed.
 
 (** *** Partial Order.
    A partial order is a preorder which is additionally antisymmetric.
diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v
index 8d790d1fd..75bf27702 100644
--- a/theories/Init/Datatypes.v
+++ b/theories/Init/Datatypes.v
@@ -226,6 +226,35 @@ Qed.
 Definition ID := forall A:Type, A -> A.
 Definition id : ID := fun A x => x.
 
+(** Polymorphic lists and some operations *)
+
+Inductive list (A : Type) : Type :=
+ | nil : list A
+ | cons : A -> list A -> list A.
+
+Implicit Arguments nil [A].
+Infix "::" := cons (at level 60, right associativity) : list_scope.
+Delimit Scope list_scope with list.
+Bind Scope list_scope with list.
+
+Local Open Scope list_scope.
+
+Fixpoint length (A : Type) (l:list A) : nat :=
+  match l with
+   | nil => O
+   | _ :: l' => S (length l')
+  end.
+
+(** Concatenation of two lists *)
+
+Fixpoint app (A : Type) (l m:list A) : list A :=
+  match l with
+   | nil => m
+   | a :: l1 => a :: app l1 m
+  end.
+
+Infix "++" := app (right associativity, at level 60) : list_scope.
+
 (* begin hide *)
 
 (* Compatibility *)
diff --git a/theories/Lists/List.v b/theories/Lists/List.v
index 37802d4bc..01b1c066a 100644
--- a/theories/Lists/List.v
+++ b/theories/Lists/List.v
@@ -17,79 +17,43 @@ Set Implicit Arguments.
 (** * Basics: definition of polymorphic lists and some operations *)
 (******************************************************************)
 
-(** ** Definitions *)
+(** The definition of [list] is now in [Init/Datatypes],
+    as well as the definitions of [length] and [app] *)
+
+Open Scope list_scope.
 
 Section Lists.
 
   Variable A : Type.
 
-  Inductive list : Type :=
-    | nil : list
-    | cons : A -> list -> list.
-
-  Infix "::" := cons (at level 60, right associativity) : list_scope.
-
-  Open Scope list_scope.
-
   (** Head and tail        *)
-  Definition head (l:list) :=
+  Definition head (l:list A) :=
     match l with
       | nil => error
       | x :: _ => value x
     end.
 
- Definition hd (default:A) (l:list) :=
+ Definition hd (default:A) (l:list A) :=
    match l with
      | nil => default
      | x :: _ => x
    end.
 
-  Definition tail (l:list) : list :=
+  Definition tail (l:list A) : list A :=
     match l with
       | nil => nil
       | a :: m => m
     end.
 
-  (** Length of lists                *)
-  Fixpoint length (l:list) : nat :=
-    match l with
-      | nil => 0
-      | _ :: m => S (length m)
-    end.
-
   (** The [In] predicate *)
-  Fixpoint In (a:A) (l:list) {struct l} : Prop :=
+  Fixpoint In (a:A) (l:list A) : Prop :=
     match l with
       | nil => False
       | b :: m => b = a \/ In a m
     end.
 
-
-  (** Concatenation of two lists *)
-  Fixpoint app (l m:list) {struct l} : list :=
-    match l with
-      | nil => m
-      | a :: l1 => a :: app l1 m
-    end.
-
-  Infix "++" := app (right associativity, at level 60) : list_scope.
-
 End Lists.
 
-(** Exporting list notations and tactics *)
-
-Implicit Arguments nil [A].
-Infix "::" := cons (at level 60, right associativity) : list_scope.
-Infix "++" := app (right associativity, at level 60) : list_scope.
-
-Open Scope list_scope.
-
-Delimit Scope list_scope with list.
-
-Bind Scope list_scope with list.
-
-Arguments Scope list [type_scope].
-
 (** ** Facts about lists *)
 
 Section Facts.
@@ -1950,7 +1914,19 @@ Ltac simpl_list := autorewrite with list.
 Ltac ssimpl_list := autorewrite with list using simpl.
 
 (* begin hide *)
-(* Compatibility *)
+(* Compatibility notations after the migration of [list] to [Datatypes] *)
+Notation list := list (only parsing).
+Notation list_rect := list_rect (only parsing).
+Notation list_rec := list_rec (only parsing).
+Notation list_ind := list_ind (only parsing).
+Notation nil := @nil (only parsing).
+Notation cons := @cons (only parsing).
+Notation length := @length (only parsing).
+Notation app := @app (only parsing).
+(* We hide these compatibility notations behind the true definitions
+   that are in [Datatypes]: *)
+Export Datatypes.
+(* Compatibility Names *)
 Notation ass_app := app_assoc (only parsing).
 Notation app_ass := app_assoc_reverse (only parsing).
 Hint Resolve app_nil_end : datatypes v62.
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.