Imported Upstream version 8.0pl3+8.1alphaupstream/8.0pl3+8.1alpha

7 files changed, 1141 insertions, 205 deletions

diff --git a/theories/Lists/List.v b/theories/Lists/List.v
index c3f65d67..ad91a350 100755..100644
--- a/theories/Lists/List.v
+++ b/theories/Lists/List.v
@@ -6,10 +6,9 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: List.v,v 1.9.2.1 2004/07/16 19:31:05 herbelin Exp $ i*)
-
-Require Import Le.
+(*i $Id: List.v 8686 2006-04-06 13:25:10Z letouzey $ i*)
 
+Require Import Le Minus Min Bool.
 
 Section Lists.
 
@@ -25,6 +24,8 @@ Infix "::" := cons (at level 60, right associativity) : list_scope.
 
 Open Scope list_scope.
 
+Ltac now_show c := change c in |- *.
+
 (*************************)
 (** Discrimination       *)
 (*************************)
@@ -35,108 +36,6 @@ Proof.
 Qed.
 
 (*************************)
-(** Concatenation        *)
-(*************************)
-
-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.
-
-Lemma app_nil_end : forall l:list, l = l ++ nil.
-Proof. 
-	induction l; simpl in |- *; auto.
-        rewrite <- IHl; auto.
-Qed.
-Hint Resolve app_nil_end.
-
-Ltac now_show c := change c in |- *.
-
-Lemma app_ass : forall l m n:list, (l ++ m) ++ n = l ++ m ++ n.
-Proof. 
-	intros. induction l; simpl in |- *; auto.
-        now_show (a :: (l ++ m) ++ n = a :: l ++ m ++ n).
-	rewrite <- IHl; auto.
-Qed.
-Hint Resolve app_ass.
-
-Lemma ass_app : forall l m n:list, l ++ m ++ n = (l ++ m) ++ n.
-Proof. 
-	auto.
-Qed.
-Hint Resolve ass_app.
-
-Lemma app_comm_cons : forall (x y:list) (a:A), a :: x ++ y = (a :: x) ++ y.
-Proof.
- auto.
-Qed.
-
-Lemma app_eq_nil : forall x y:list, x ++ y = nil -> x = nil /\ y = nil.
-Proof.
-  destruct x as [| a l]; [ destruct y as [| a l] | destruct y as [| a0 l0] ];
-   simpl in |- *; auto.
-  intros H; discriminate H.
-  intros; discriminate H.
-Qed.
-
-Lemma app_cons_not_nil : forall (x y:list) (a:A), nil <> x ++ a :: y.
-Proof.
-unfold not in |- *.
-  destruct x as [| a l]; simpl in |- *; intros.
-  discriminate H.
-  discriminate H.
-Qed.
-
-Lemma app_eq_unit :
- forall (x y:list) (a:A),
-   x ++ y = a :: nil -> x = nil /\ y = a :: nil \/ x = a :: nil /\ y = nil.
-
-Proof.
-  destruct x as [| a l]; [ destruct y as [| a l] | destruct y as [| a0 l0] ];
-   simpl in |- *.
-  intros a H; discriminate H.
-  left; split; auto.
-  right; split; auto.
-  generalize H.
-  generalize (app_nil_end l); intros E.
-  rewrite <- E; auto.
-  intros.
-  injection H.
-  intro.
-  cut (nil = l ++ a0 :: l0); auto.
-  intro.
-  generalize (app_cons_not_nil _ _ _ H1); intro.
-  elim H2.
-Qed.
-
-Lemma app_inj_tail :
- forall (x y:list) (a b:A), x ++ a :: nil = y ++ b :: nil -> x = y /\ a = b.
-Proof.
-  induction x as [| x l IHl];
-   [ destruct y as [| a l] | destruct y as [| a l0] ]; 
-   simpl in |- *; auto.
-  intros a b H.
-  injection H.
-  auto.
-  intros a0 b H.
-  injection H; intros.
-  generalize (app_cons_not_nil _ _ _ H0); destruct 1.
-  intros a b H.
-  injection H; intros.
-  cut (nil = l ++ a :: nil); auto.
-  intro.
-  generalize (app_cons_not_nil _ _ _ H2); destruct 1.
-  intros a0 b H.
-  injection H; intros.
-  destruct (IHl l0 a0 b H0). 
-  split; auto.
-  rewrite <- H1; rewrite <- H2; reflexivity.
-Qed.
-
-(*************************)
 (** Head and tail        *)
 (*************************)
 
@@ -253,6 +152,189 @@ Proof.
   destruct (H a0 a); simpl in |- *; auto.
   destruct IHl; simpl in |- *; auto. 
   right; unfold not in |- *; intros [Hc1| Hc2]; auto.
+Defined.
+
+(**************************)
+(** Nth element of a list *)
+(**************************)
+
+Fixpoint nth (n:nat) (l:list) (default:A) {struct l} : A :=
+  match n, l with
+  | O, x :: l' => x
+  | O, other => default
+  | S m, nil => default
+  | S m, x :: t => nth m t default
+  end.
+
+Fixpoint nth_ok (n:nat) (l:list) (default:A) {struct l} : bool :=
+  match n, l with
+  | O, x :: l' => true
+  | O, other => false
+  | S m, nil => false
+  | S m, x :: t => nth_ok m t default
+  end.
+
+Lemma nth_in_or_default :
+ forall (n:nat) (l:list) (d:A), {In (nth n l d) l} + {nth n l d = d}.
+(* Realizer nth_ok. Program_all. *)
+Proof. 
+  intros n l d; generalize n; induction l; intro n0.
+  right; case n0; trivial.
+  case n0; simpl in |- *.
+  auto.
+  intro n1; elim (IHl n1); auto.     
+Qed.
+
+Lemma nth_S_cons :
+ forall (n:nat) (l:list) (d a:A),
+   In (nth n l d) l -> In (nth (S n) (a :: l) d) (a :: l).
+Proof. 
+  simpl in |- *; auto.
+Qed.
+
+Fixpoint nth_error (l:list) (n:nat) {struct n} : Exc A :=
+  match n, l with
+  | O, x :: _ => value x
+  | S n, _ :: l => nth_error l n
+  | _, _ => error
+  end.
+
+Definition nth_default (default:A) (l:list) (n:nat) : A :=
+  match nth_error l n with
+  | Some x => x
+  | None => default
+  end.
+
+Lemma nth_In :
+ forall (n:nat) (l:list) (d:A), n < length l -> In (nth n l d) l.
+
+Proof.
+unfold lt in |- *; induction n as [| n hn]; simpl in |- *.
+destruct l; simpl in |- *; [ inversion 2 | auto ].
+destruct l as [| a l hl]; simpl in |- *.
+inversion 2.
+intros d ie; right; apply hn; auto with arith.
+Qed.
+
+Lemma nth_overflow : forall l n d, length l <= n -> nth n l d = d.
+Proof.
+induction l; destruct n; simpl; intros; auto.
+inversion H.
+apply IHl; auto with arith.
+Qed.
+
+Lemma nth_indep : 
+ forall l n d d', n < length l -> nth n l d = nth n l d'.
+Proof.
+induction l; simpl; intros; auto.
+inversion H.
+destruct n; simpl; auto with arith.
+Qed.
+
+
+(*************************)
+(** Concatenation        *)
+(*************************)
+
+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.
+
+Lemma app_nil_end : forall l:list, l = l ++ nil.
+Proof. 
+	induction l; simpl in |- *; auto.
+        rewrite <- IHl; auto.
+Qed.
+Hint Resolve app_nil_end.
+
+Lemma app_ass : forall l m n:list, (l ++ m) ++ n = l ++ m ++ n.
+Proof. 
+	intros. induction l; simpl in |- *; auto.
+        now_show (a :: (l ++ m) ++ n = a :: l ++ m ++ n).
+	rewrite <- IHl; auto.
+Qed.
+Hint Resolve app_ass.
+
+Lemma ass_app : forall l m n:list, l ++ m ++ n = (l ++ m) ++ n.
+Proof. 
+	auto.
+Qed.
+Hint Resolve ass_app.
+
+Lemma app_comm_cons : forall (x y:list) (a:A), a :: x ++ y = (a :: x) ++ y.
+Proof.
+ auto.
+Qed.
+
+Lemma app_eq_nil : forall x y:list, x ++ y = nil -> x = nil /\ y = nil.
+Proof.
+  destruct x as [| a l]; [ destruct y as [| a l] | destruct y as [| a0 l0] ];
+   simpl in |- *; auto.
+  intros H; discriminate H.
+  intros; discriminate H.
+Qed.
+
+Lemma app_cons_not_nil : forall (x y:list) (a:A), nil <> x ++ a :: y.
+Proof.
+unfold not in |- *.
+  destruct x as [| a l]; simpl in |- *; intros.
+  discriminate H.
+  discriminate H.
+Qed.
+
+Lemma app_eq_unit :
+ forall (x y:list) (a:A),
+   x ++ y = a :: nil -> x = nil /\ y = a :: nil \/ x = a :: nil /\ y = nil.
+
+Proof.
+  destruct x as [| a l]; [ destruct y as [| a l] | destruct y as [| a0 l0] ];
+   simpl in |- *.
+  intros a H; discriminate H.
+  left; split; auto.
+  right; split; auto.
+  generalize H.
+  generalize (app_nil_end l); intros E.
+  rewrite <- E; auto.
+  intros.
+  injection H.
+  intro.
+  cut (nil = l ++ a0 :: l0); auto.
+  intro.
+  generalize (app_cons_not_nil _ _ _ H1); intro.
+  elim H2.
+Qed.
+
+Lemma app_inj_tail :
+ forall (x y:list) (a b:A), x ++ a :: nil = y ++ b :: nil -> x = y /\ a = b.
+Proof.
+  induction x as [| x l IHl];
+   [ destruct y as [| a l] | destruct y as [| a l0] ]; 
+   simpl in |- *; auto.
+  intros a b H.
+  injection H.
+  auto.
+  intros a0 b H.
+  injection H; intros.
+  generalize (app_cons_not_nil _ _ _ H0); destruct 1.
+  intros a b H.
+  injection H; intros.
+  cut (nil = l ++ a :: nil); auto.
+  intro.
+  generalize (app_cons_not_nil _ _ _ H2); destruct 1.
+  intros a0 b H.
+  injection H; intros.
+  destruct (IHl l0 a0 b H0). 
+  split; auto.
+  rewrite <- H1; rewrite <- H2; reflexivity.
+Qed.
+
+Lemma app_length : forall l l', length (l++l') = length l + length l'.
+Proof.
+induction l; simpl; auto.
 Qed.
 
 Lemma in_app_or : forall (l m:list) (a:A), In a (l ++ m) -> In a l \/ In a m.
@@ -285,6 +367,33 @@ Proof.
 Qed.
 Hint Resolve in_or_app.
 
+Lemma app_nth1 : 
+ forall l l' d n, n < length l -> nth n (l++l') d = nth n l d.
+Proof.
+induction l.
+intros.
+inversion H.
+intros l' d n.
+case n; simpl; auto.
+intros; rewrite IHl; auto with arith.
+Qed.
+
+Lemma app_nth2 : 
+ forall l l' d n, n >= length l -> nth n (l++l') d = nth (n-length l) l' d.
+Proof.
+induction l.
+intros.
+simpl.
+destruct n; auto.
+intros l' d n.
+case n; simpl; auto.
+intros.
+inversion H.
+intros.
+rewrite IHl; auto with arith.
+Qed.
+
+
 (***************************)
 (** Set inclusion on list  *)
 (***************************)
@@ -344,67 +453,7 @@ Proof.
 Qed.
 Hint Resolve incl_app.
 
-(**************************)
-(** Nth element of a list *)
-(**************************)
-
-Fixpoint nth (n:nat) (l:list) (default:A) {struct l} : A :=
-  match n, l with
-  | O, x :: l' => x
-  | O, other => default
-  | S m, nil => default
-  | S m, x :: t => nth m t default
-  end.
-
-Fixpoint nth_ok (n:nat) (l:list) (default:A) {struct l} : bool :=
-  match n, l with
-  | O, x :: l' => true
-  | O, other => false
-  | S m, nil => false
-  | S m, x :: t => nth_ok m t default
-  end.
-
-Lemma nth_in_or_default :
- forall (n:nat) (l:list) (d:A), {In (nth n l d) l} + {nth n l d = d}.
-(* Realizer nth_ok. Program_all. *)
-Proof. 
-  intros n l d; generalize n; induction l; intro n0.
-  right; case n0; trivial.
-  case n0; simpl in |- *.
-  auto.
-  intro n1; elim (IHl n1); auto.     
-Qed.
-
-Lemma nth_S_cons :
- forall (n:nat) (l:list) (d a:A),
-   In (nth n l d) l -> In (nth (S n) (a :: l) d) (a :: l).
-Proof. 
-  simpl in |- *; auto.
-Qed.
 
-Fixpoint nth_error (l:list) (n:nat) {struct n} : Exc A :=
-  match n, l with
-  | O, x :: _ => value x
-  | S n, _ :: l => nth_error l n
-  | _, _ => error
-  end.
-
-Definition nth_default (default:A) (l:list) (n:nat) : A :=
-  match nth_error l n with
-  | Some x => x
-  | None => default
-  end.
-
-Lemma nth_In :
- forall (n:nat) (l:list) (d:A), n < length l -> In (nth n l d) l.
-
-Proof.
-unfold lt in |- *; induction n as [| n hn]; simpl in |- *.
-destruct l; simpl in |- *; [ inversion 2 | auto ].
-destruct l as [| a l hl]; simpl in |- *.
-inversion 2.
-intros d ie; right; apply hn; auto with arith.
-Qed.
 
 (********************************)
 (** Decidable equality on lists *)
@@ -466,6 +515,72 @@ Proof.
  rewrite IHl; auto.
 Qed.
 
+Lemma In_rev : forall l x, In x l <-> In x (rev l).
+Proof.
+induction l.
+simpl; intuition.
+intros.
+simpl.
+intuition.
+subst.
+apply in_or_app; right; simpl; auto.
+apply in_or_app; left; firstorder.
+destruct (in_app_or _ _ _ H); firstorder.
+Qed.
+
+Lemma rev_length : forall l, length (rev l) = length l.
+Proof.
+induction l;simpl; auto.
+rewrite app_length.
+rewrite IHl.
+simpl.
+elim (length l); simpl; auto.
+Qed.
+
+Lemma rev_nth : forall l d n,  n < length l ->  
+ nth n (rev l) d = nth (length l - S n) l d.
+Proof.
+induction l.
+intros; inversion H.
+intros.
+simpl in H.
+simpl (rev (a :: l)).
+simpl (length (a :: l) - S n).
+inversion H.
+rewrite <- minus_n_n; simpl.
+rewrite <- rev_length.
+rewrite app_nth2; auto.
+rewrite <- minus_n_n; auto.
+rewrite app_nth1; auto.
+rewrite (minus_plus_simpl_l_reverse (length l) n 1).
+replace (1 + length l) with (S (length l)); auto with arith.
+rewrite <- minus_Sn_m; auto with arith; simpl.
+apply IHl; auto.
+rewrite rev_length; auto.
+Qed.
+
+(****************************************************)
+(**  An alternative tail-recursive definition for reverse *) 
+(****************************************************)
+
+Fixpoint rev_acc (l l': list) {struct l} : list := 
+ match l with 
+  | nil => l' 
+  | a::l => rev_acc l (a::l')
+ end.
+
+Lemma rev_acc_rev : forall l l', rev_acc l l' = rev l ++ l'.
+Proof.
+induction l; simpl; auto; intros.
+rewrite <- ass_app; firstorder.
+Qed.
+
+Lemma rev_alt : forall l, rev l = rev_acc l nil.
+Proof.
+intros; rewrite rev_acc_rev.
+apply app_nil_end.
+Qed.
+
 (*********************************************)
 (**  Reverse Induction Principle on Lists    *)
 (*********************************************)
@@ -503,9 +618,119 @@ Qed.
 
 End Reverse_Induction.
 
+(***************************)
+(** Last elements of a list *)
+(***************************)
+
+(** [last l d] returns the last elements of the list [l], 
+    or the default value [d] if [l] is empty. *)
+
+Fixpoint last (l:list)(d:A)  {struct l} : A := 
+ match l with 
+  | nil => d 
+  | a :: nil => a 
+  | a :: l => last l d
+ end.
+
+(** [removelast l] remove the last element of [l] *)
+
+Fixpoint removelast (l:list) {struct l} : list := 
+ match l with 
+  | nil =>  nil 
+  | a :: nil => nil 
+  | a :: l => a :: removelast l
+ end.
+
+Lemma app_removelast_last : 
+ forall l d, l<>nil -> l = removelast l ++ (last l d :: nil).
+Proof.
+induction l.
+destruct 1; auto.
+intros d _.
+destruct l; auto.
+pattern (a0::l) at 1; rewrite IHl with d; auto; discriminate.
+Qed.
+
+Lemma exists_last : 
+ forall l, l<>nil -> { l' : list & { a : A | l = l'++a::nil}}. 
+Proof. 
+induction l.
+destruct 1; auto.
+intros _.
+destruct l.
+exists nil; exists a; auto.
+destruct IHl as [l' (a',H)]; try discriminate.
+rewrite H.
+exists (a::l'); exists a'; auto.
+Qed.
+
+(********************************)
+(* Cutting a list at some position *)
+(********************************)
+
+Fixpoint firstn (n:nat)(l:list) {struct n} : list := 
+ match n with 
+  | 0 => nil 
+  | S n => match l with  
+       | nil => nil 
+       | a::l => a::(firstn n l)
+   end
+  end.
+
+Fixpoint skipn (n:nat)(l:list) { struct n } : list := 
+  match n with 
+   | 0 => l 
+   | S n => match l with 
+        | nil => nil 
+        | a::l => skipn n l
+    end
+  end.
+
+Lemma firstn_skipn : forall n l, firstn n l ++ skipn n l = l.
+Proof.
+induction n.
+simpl; auto.
+destruct l; simpl; auto.
+f_equal; auto.
+Qed.
+
+(**************)
+(** Remove *)
+(**************)
+
+Section Remove.
+
+Hypothesis eq_dec : forall x y : A, {x = y}+{x <> y}.
+
+Fixpoint remove (x : A) (l : list){struct l} : list :=
+  match l with
+    | nil => nil
+    | y::tl => if (eq_dec x y) then remove x tl else y::(remove x tl)
+  end.
+
+End Remove.
+
+(***************************)
+(** List without redundancy *)
+(***************************)
+
+Inductive NoDup : list -> Prop := 
+ | NoDup_nil : NoDup nil 
+ | NoDup_cons : forall x l, ~ In x l -> NoDup l -> NoDup (x::l). 
+
 End Lists.
 
+(** Exporting list notations and hints *)
+
 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.
 
 Hint Resolve nil_cons app_nil_end ass_app app_ass: datatypes v62.
 Hint Resolve app_comm_cons app_cons_not_nil: datatypes v62.
@@ -523,40 +748,241 @@ Section Functions_on_lists.
 (** Some generic functions on lists and basic functions of them *)
 (****************************************************************)
 
+(*********)
+(** Map *)
+(*********)
+
 Section Map.
 Variables A B : Set.
 Variable f : A -> B.
+
 Fixpoint map (l:list A) : list B :=
   match l with
   | nil => nil
   | cons a t => cons (f a) (map t)
   end.
-End Map.
 
 Lemma in_map :
- forall (A B:Set) (f:A -> B) (l:list A) (x:A), In x l -> In (f x) (map f l).
+ forall (l:list A) (x:A), In x l -> In (f x) (map l).
 Proof. 
   induction l as [| a l IHl]; simpl in |- *;
    [ auto
    | destruct 1; [ left; apply f_equal with (f := f); assumption | auto ] ].
 Qed.
 
-Fixpoint flat_map (A B:Set) (f:A -> list B) (l:list A) {struct l} : 
+Lemma in_map_iff : forall l y, In y (map l) <-> exists x, f x = y /\ In x l.
+Proof.
+induction l; firstorder (subst; auto).
+Qed.
+
+Lemma map_length : forall l, length (map l) = length l.
+Proof.
+induction l; simpl; auto.
+Qed.
+
+Lemma map_nth : forall l d n, 
+ nth n (map l) (f d) = f (nth n l d).
+Proof.
+induction l; simpl map; destruct n; firstorder.
+Qed.
+
+Lemma map_app : forall l l',  
+ map (l++l') = (map l)++(map l').
+Proof. 
+induction l; simpl; auto.
+intros; rewrite IHl; auto.
+Qed.
+
+Lemma map_rev : forall l, map (rev l) = rev (map l).
+Proof. 
+induction l; simpl; auto.
+rewrite map_app.
+rewrite IHl; auto.
+Qed.
+
+End Map. 
+
+Lemma map_map : forall (A B C:Set)(f:A->B)(g:B->C) l, 
+  map g (map f l) = map (fun x => g (f x)) l.
+Proof.
+induction l; simpl; auto.
+rewrite IHl; auto.
+Qed.
+
+Lemma map_ext : 
+ forall (A B : Set)(f g:A->B), (forall a, f a = g a) -> forall l, map f l = map g l.
+Proof.
+induction l; simpl; auto.
+rewrite H; rewrite IHl; auto.
+Qed.
+
+(********************************************)
+(** Operations on lists of pairs or lists of lists *)
+(********************************************)
+
+Section ListPairs.
+Variable A B : Set.
+
+(** [split] derives two lists from a list of pairs *)
+
+Fixpoint split  (l:list (A*B)) { struct l }: list A * list B :=
+  match l with
+    | nil => (nil, nil)
+    | (x,y) :: tl => let (g,d) := split tl in (x::g, y::d)
+  end.
+
+Lemma in_split_l : forall (l:list (A*B))(p:A*B), 
+  In p l -> In (fst p) (fst (split l)). 
+Proof.
+induction l; simpl; intros; auto.
+destruct p; destruct a; destruct (split l); simpl in *.
+destruct H.
+injection H; auto.
+right; apply (IHl (a0,b) H).
+Qed.
+
+Lemma in_split_r : forall (l:list (A*B))(p:A*B), 
+  In p l -> In (snd p) (snd (split l)). 
+Proof.
+induction l; simpl; intros; auto.
+destruct p; destruct a; destruct (split l); simpl in *.
+destruct H.
+injection H; auto.
+right; apply (IHl (a0,b) H).
+Qed.
+
+Lemma split_nth : forall (l:list (A*B))(n:nat)(d:A*B), 
+ nth n l d = (nth n (fst (split l)) (fst d), nth n (snd (split l)) (snd d)).
+Proof.
+induction l.
+destruct n; destruct d; simpl; auto.
+destruct n; destruct d; simpl; auto.
+destruct a; destruct (split l); simpl; auto.
+destruct a; destruct (split l); simpl in *; auto.
+rewrite IHl; simpl; auto.
+Qed.
+
+Lemma split_lenght_l : forall (l:list (A*B)),
+  length (fst (split l)) = length l. 
+Proof.
+induction l; simpl; auto.
+destruct a; destruct (split l); simpl; auto.
+Qed.
+
+Lemma split_lenght_r : forall (l:list (A*B)),
+  length (snd (split l)) = length l. 
+Proof.
+induction l; simpl; auto.
+destruct a; destruct (split l); simpl; auto.
+Qed.
+
+(** [combine] is the opposite of [split]. 
+    Lists given to [combine] are meant to be of same length. 
+    If not, [combine] stops on the shorter list *)
+
+Fixpoint combine (l : list A) (l' : list B){struct l} : list (A*B) :=
+  match l,l' with
+    | x::tl, y::tl' => (x,y)::(combine tl tl')
+    | _, _ => nil
+  end.
+
+Lemma split_combine : forall (l: list (A*B)), 
+  let (l1,l2) := split l in combine l1 l2 = l.
+Proof.
+induction l.
+simpl; auto.
+destruct a; simpl. 
+destruct (split l); simpl in *.
+f_equal; auto.
+Qed.
+
+Lemma combine_split : forall (l:list A)(l':list B), length l = length l' -> 
+ split (combine l l') = (l,l').
+Proof.
+induction l; destruct l'; simpl; intros; auto; try discriminate.
+injection H; clear H; intros.
+rewrite IHl; auto.
+Qed.
+
+Lemma in_combine_l : forall (l:list A)(l':list B)(x:A)(y:B), 
+ In (x,y) (combine l l') -> In x l.
+Proof.
+induction l.
+simpl; auto.
+destruct l'; simpl; auto; intros.
+contradiction. 
+destruct H.
+injection H; auto.
+right; apply IHl with l' y; auto.
+Qed.
+
+Lemma in_combine_r : forall (l:list A)(l':list B)(x:A)(y:B), 
+ In (x,y) (combine l l') -> In y l'.
+Proof.
+induction l.
+simpl; intros; contradiction.
+destruct l'; simpl; auto; intros.
+destruct H.
+injection H; auto.
+right; apply IHl with x; auto.
+Qed.
+
+Lemma combine_length : forall (l:list A)(l':list B), 
+  length (combine l l') = min (length l) (length l').
+Proof.
+induction l.
+simpl; auto.
+destruct l'; simpl; auto.
+Qed.
+
+Lemma combine_nth : forall (l:list A)(l':list B)(n:nat)(x:A)(y:B), 
+ length l = length l' -> 
+ nth n (combine l l') (x,y) = (nth n l x, nth n l' y).
+Proof.
+induction l; destruct l'; intros; try discriminate.
+destruct n; simpl; auto.
+destruct n; simpl in *; auto.
+Qed.
+
+(** [flat_map] *)
+
+Fixpoint flat_map (f:A -> list B) (l:list A) {struct l} : 
  list B :=
   match l with
   | nil => nil
-  | cons x t => app (f x) (flat_map f t)
+  | cons x t => (f x)++(flat_map f t)
   end.
 
-Fixpoint list_prod (A B:Set) (l:list A) (l':list B) {struct l} :
+Lemma in_flat_map : forall (f:A->list B)(l:list A)(y:B),
+ In y (flat_map f l) <-> exists x, In x l /\ In y (f x). 
+Proof.
+induction l; simpl; split; intros.
+contradiction.
+destruct H as (x,(H,_)); contradiction.
+destruct (in_app_or _ _ _ H).
+exists a; auto.
+destruct (IHl y) as (H1,_); destruct (H1 H0) as (x,(H2,H3)).
+exists x; auto.
+apply in_or_app.
+destruct H as (x,(H0,H1)); destruct H0.
+subst; auto.
+right; destruct (IHl y) as (_,H2); apply H2.
+exists x; auto.
+Qed.
+
+(** [list_prod] has the same signature as [combine], but unlike
+   [combine], it adds every possible pairs, not only those at the 
+   same position. *)
+
+Fixpoint list_prod (l:list A) (l':list B) {struct l} :
  list (A * B) :=
   match l with
   | nil => nil
-  | cons x t => app (map (fun y:B => (x, y)) l') (list_prod t l')
+  | cons x t => (map (fun y:B => (x, y)) l')++(list_prod t l')
   end.
 
 Lemma in_prod_aux :
- forall (A B:Set) (x:A) (y:B) (l:list B),
+ forall (x:A) (y:B) (l:list B),
    In y l -> In (x, y) (map (fun y0:B => (x, y0)) l).
 Proof. 
   induction l;
@@ -566,7 +992,7 @@ Proof.
 Qed.
 
 Lemma in_prod :
- forall (A B:Set) (l:list A) (l':list B) (x:A) (y:B),
+ forall (l:list A) (l':list B) (x:A) (y:B),
    In x l -> In y l' -> In (x, y) (list_prod l l').
 Proof. 
   induction l;
@@ -575,10 +1001,36 @@ Proof.
       [ left; rewrite H; apply in_prod_aux; assumption | right; auto ] ].
 Qed.
 
+Lemma in_prod_iff : 
+ forall (l:list A)(l':list B)(x:A)(y:B), 
+  In (x,y) (list_prod l l') <-> In x l /\ In y l'.
+Proof.
+split; [ | intros; apply in_prod; intuition ].
+induction l; simpl; intros.
+intuition.
+destruct (in_app_or _ _ _ H); clear H.
+destruct (in_map_iff (fun y : B => (a, y)) l' (x,y)) as (H1,_).
+destruct (H1 H0) as (z,(H2,H3)); clear H0 H1.
+injection H2; clear H2; intros; subst; intuition.
+intuition.
+Qed. 
+
+Lemma prod_length : forall (l:list A)(l':list B), 
+  length (list_prod l l') = (length l) * (length l').
+Proof.
+induction l; simpl; auto.
+intros.
+rewrite app_length.
+rewrite map_length.
+auto.
+Qed.
+
+End ListPairs.
+
 (** [(list_power x y)] is [y^x], or the set of sequences of elts of [y]
     indexed by elts of [x], sorted in lexicographic order. *)
 
-Fixpoint list_power (A B:Set) (l:list A) (l':list B) {struct l} :
+Fixpoint list_power (A B:Set)(l:list A) (l':list B) {struct l} :
  list (list (A * B)) :=
   match l with
   | nil => cons nil nil
@@ -594,13 +1046,37 @@ Fixpoint list_power (A B:Set) (l:list A) (l':list B) {struct l} :
 Section Fold_Left_Recursor.
 Variables A B : Set.
 Variable f : A -> B -> A.
+
 Fixpoint fold_left (l:list B) (a0:A) {struct l} : A :=
   match l with
   | nil => a0
   | cons b t => fold_left t (f a0 b)
   end.
+
+Lemma fold_left_app : forall (l l':list B)(i:A), 
+ fold_left (l++l') i = fold_left l' (fold_left l i).
+Proof.
+induction l. 
+simpl; auto.
+intros.
+simpl.
+auto.
+Qed.
+
 End Fold_Left_Recursor.
 
+Lemma fold_left_length : 
+ forall (A:Set)(l:list A), fold_left (fun x _ => S x) l 0 = length l.
+Proof.
+intro A.
+cut (forall (l:list A) n, fold_left (fun x _ => S x) l n = n + length l).
+intros.
+exact (H l 0).
+induction l; simpl; auto.
+intros; rewrite IHl.
+simpl; auto with arith.
+Qed.
+
 (************************************)
 (** Right-to-left iterator on lists *)
 (************************************)
@@ -609,13 +1085,34 @@ Section Fold_Right_Recursor.
 Variables A B : Set.
 Variable f : B -> A -> A.
 Variable a0 : A.
+
 Fixpoint fold_right (l:list B) : A :=
   match l with
   | nil => a0
   | cons b t => f b (fold_right t)
   end.
+
 End Fold_Right_Recursor.
 
+Lemma fold_right_app : forall (A B:Set)(f:A->B->B) l l' i, 
+  fold_right f i (l++l') = fold_right f (fold_right f i l') l.
+Proof.
+induction l.
+simpl; auto.
+simpl; intros.
+f_equal; auto.
+Qed.
+
+Lemma fold_left_rev_right : forall (A B:Set)(f:A->B->B) l i, 
+  fold_right f i (rev l) = fold_left (fun x y => f y x) l i.
+Proof.
+induction l.
+simpl; auto.
+intros.
+simpl.
+rewrite fold_right_app; simpl; auto.
+Qed.
+
 Theorem fold_symmetric :
  forall (A:Set) (f:A -> A -> A),
    (forall x y z:A, f x (f y z) = f (f x y) z) ->
@@ -638,18 +1135,157 @@ rewrite IHl.
 reflexivity.
 Qed.
 
-End Functions_on_lists.
+(********************************)
+(** Boolean operations over lists *)
+(********************************)
 
+Section Bool. 
+Variable A : Set.
+Variable f : A -> bool.
 
-(** Exporting list notations *)
+(** find whether a boolean function can be satisfied by an 
+     elements of the list. *)
 
-Infix "::" := cons (at level 60, right associativity) : list_scope.
+Fixpoint existsb (l:list A) {struct l}: bool := 
+ match l with 
+    | nil => false
+    | a::l => f a || existsb l
+ end.
 
-Infix "++" := app (right associativity, at level 60) : list_scope.
+Lemma existsb_exists : 
+ forall l, existsb l = true <-> exists x, In x l /\ f x = true.
+Proof.
+induction l; simpl; intuition.
+inversion H.
+firstorder.
+destruct (orb_prop _ _ H1); firstorder.
+firstorder.
+subst.
+rewrite H2; auto.
+Qed.
 
-Open Scope list_scope.
+Lemma existsb_nth : forall l n d, n < length l ->
+  existsb l = false -> f (nth n l d) = false.
+Proof.
+induction l.
+inversion 1.
+simpl; intros.
+destruct (orb_false_elim _ _ H0); clear H0; auto.
+destruct n ; auto. 
+rewrite IHl; auto with arith.
+Qed.
 
-(** Declare Scope list_scope with key list *)
-Delimit Scope list_scope with list.
+(** find whether a boolean function is satisfied by 
+  all the elements of a list. *)
 
-Bind Scope list_scope with list.
+Fixpoint forallb (l:list A) {struct l} : bool := 
+ match l with 
+    | nil => true
+    | a::l => f a && forallb l
+ end.
+
+Lemma forallb_forall : 
+ forall l, forallb l = true <-> (forall x, In x l -> f x = true).
+Proof.
+induction l; simpl; intuition.
+destruct (andb_prop _ _ H1).
+congruence.
+destruct (andb_prop _ _ H1); auto.
+assert (forallb l = true).
+apply H0; intuition.
+rewrite H1; auto. 
+Qed.
+
+(** [filter] *)
+
+Fixpoint filter (l:list A) : list A := 
+ match l with 
+  | nil => nil
+  | x :: l => if f x then x::(filter l) else filter l
+ end.
+
+Lemma filter_In : forall x l, In x (filter l) <-> In x l /\ f x = true.
+Proof.
+induction l; simpl.
+intuition.
+intros.
+case_eq (f a); intros; simpl; intuition congruence.
+Qed.
+
+(** [find] *)
+
+Fixpoint find (l:list A) : option A :=
+  match l with
+    | nil => None
+    | x :: tl => if f x then Some x else find tl
+  end.
+
+(** [partition] *)
+
+Fixpoint partition (l:list A) {struct l} : list A * list A := 
+  match l with
+    | nil => (nil, nil)
+    | x :: tl => let (g,d) := partition tl in 
+      if f x then (x::g,d) else (g,x::d)
+  end.
+
+End Bool.
+
+
+(*********************************)
+(** Sequence of natural numbers *)
+(*********************************)
+
+(** [seq] computes the sequence of [len] contiguous integers 
+    that starts at [start]. For instance, [seq 2 3] is [2::3::4::nil]. *)
+
+Fixpoint seq (start len:nat) {struct len} : list nat := 
+ match len with 
+  | 0 => nil
+  | S len => start :: seq (S start) len
+ end. 
+
+Lemma seq_length : forall len start, length (seq start len) = len.
+Proof.
+induction len; simpl; auto.
+Qed.
+
+Lemma seq_nth : forall len start n d, 
+  n < len -> nth n (seq start len) d = start+n.
+Proof.
+induction len; intros.
+inversion H.
+simpl seq.
+destruct n; simpl.
+auto with arith.
+rewrite IHlen;simpl; auto with arith.
+Qed.
+
+Lemma seq_shift : forall len start,
+ map S (seq start len) = seq (S start) len.
+Proof. 
+induction len; simpl; auto.
+intros.
+rewrite IHlen.
+auto with arith.
+Qed.
+
+End Functions_on_lists.
+
+
+Hint Rewrite 
+ rev_involutive (* rev (rev l) = l *)
+ rev_unit (* rev (l ++ a :: nil) = a :: rev l *)
+ map_nth (* nth n (map f l) (f d) = f (nth n l d) *)
+ map_length (* length (map f l) = length l *)
+ seq_length (* length (seq start len) = len *)
+ app_length (* length (l ++ l') = length l + length l' *)
+ rev_length (* length (rev l) = length l *)
+ : list.
+
+Hint Rewrite <- 
+ app_nil_end (* l = l ++ nil *)
+ : list.
+
+Ltac simpl_list := autorewrite with list.
+Ltac ssimpl_list := autorewrite with list using simpl.
diff --git a/theories/Lists/ListSet.v b/theories/Lists/ListSet.v
index d5ecad9c..4e009ed5 100644
--- a/theories/Lists/ListSet.v
+++ b/theories/Lists/ListSet.v
@@ -6,14 +6,12 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: ListSet.v,v 1.13.2.1 2004/07/16 19:31:05 herbelin Exp $ i*)
+(*i $Id: ListSet.v 6844 2005-03-16 13:09:55Z herbelin $ i*)
 
-(** A Library for finite sets, implemented as lists 
-    A Library with similar interface will soon be available under
-    the name TreeSet in the theories/Trees directory *)
+(** A Library for finite sets, implemented as lists *)
 
-(** PolyList is loaded, but not exported.
-    This allow to "hide" the definitions, functions and theorems of PolyList
+(** List is loaded, but not exported.
+    This allow to "hide" the definitions, functions and theorems of List
     and to see only the ones of ListSet *)
 
 Require Import List.
@@ -395,4 +393,4 @@ Section other_definitions.
  
 End other_definitions.
 
-Unset Implicit Arguments.
\ No newline at end of file
+Unset Implicit Arguments.
diff --git a/theories/Lists/MonoList.v b/theories/Lists/MonoList.v
index d639a39d..aa2b74dd 100755..100644
--- a/theories/Lists/MonoList.v
+++ b/theories/Lists/MonoList.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: MonoList.v,v 1.2.2.1 2004/07/16 19:31:05 herbelin Exp $ i*)
+(*i $Id: MonoList.v 8642 2006-03-17 10:09:02Z notin $ i*)
 
 (** THIS IS A OLD CONTRIB. IT IS NO LONGER MAINTAINED ***)
 
diff --git a/theories/Lists/SetoidList.v b/theories/Lists/SetoidList.v
new file mode 100644
index 00000000..811dcab4
--- /dev/null
+++ b/theories/Lists/SetoidList.v
@@ -0,0 +1,300 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(* $Id: SetoidList.v 8686 2006-04-06 13:25:10Z letouzey $ *)
+
+Require Export List.
+Require Export Sorting.
+Require Export Setoid.
+Set Implicit Arguments.
+Unset Strict Implicit.
+
+(** * Logical relations over lists with respect to a setoid equality 
+      or ordering. *) 
+
+(** This can be seen as a complement of predicate [lelistA] and [sort] 
+    found in [Sorting]. *)
+
+Section Type_with_equality.
+Variable A : Set.
+Variable eqA : A -> A -> Prop. 
+
+(** Being in a list modulo an equality relation over type [A]. *)
+
+Inductive InA (x : A) : list A -> Prop :=
+  | InA_cons_hd : forall y l, eqA x y -> InA x (y :: l)
+  | InA_cons_tl : forall y l, InA x l -> InA x (y :: l).
+
+Hint Constructors InA.
+
+(** An alternative definition of [InA]. *)
+
+Lemma InA_alt : forall x l, InA x l <-> exists y, eqA x y /\ In y l.
+Proof. 
+ induction l; intuition.
+ inversion H.
+ firstorder.
+ inversion H1; firstorder.
+ firstorder; subst; auto.
+Qed.
+
+(** A list without redundancy modulo the equality over [A]. *)
+
+Inductive NoDupA : list A -> Prop :=
+  | NoDupA_nil : NoDupA nil
+  | NoDupA_cons : forall x l, ~ InA x l -> NoDupA l -> NoDupA (x::l).
+
+Hint Constructors NoDupA.
+
+(** lists with same elements modulo [eqA] *)
+
+Definition eqlistA l l' := forall x, InA x l <-> InA x l'.
+
+(** Results concerning lists modulo [eqA] *)
+
+Hypothesis eqA_refl : forall x, eqA x x.
+Hypothesis eqA_sym : forall x y, eqA x y -> eqA y x.
+Hypothesis eqA_trans : forall x y z, eqA x y -> eqA y z -> eqA x z.
+
+Hint Resolve eqA_refl eqA_trans.
+Hint Immediate eqA_sym.
+
+Lemma InA_eqA : forall l x y, eqA x y -> InA x l -> InA y l.
+Proof. 
+ intros s x y.
+ do 2 rewrite InA_alt.
+ intros H (z,(U,V)).  
+ exists z; split; eauto.
+Qed.
+Hint Immediate InA_eqA.
+
+Lemma In_InA : forall l x, In x l -> InA x l.
+Proof.
+ simple induction l; simpl in |- *; intuition.
+ subst; auto.  
+Qed.
+Hint Resolve In_InA.
+
+(** Results concerning lists modulo [eqA] and [ltA] *)
+
+Variable ltA : A -> A -> Prop.
+
+Hypothesis ltA_trans : forall x y z, ltA x y -> ltA y z -> ltA x z.
+Hypothesis ltA_not_eqA : forall x y, ltA x y -> ~ eqA x y.
+Hypothesis ltA_eqA : forall x y z, ltA x y -> eqA y z -> ltA x z.
+Hypothesis eqA_ltA : forall x y z, eqA x y -> ltA y z -> ltA x z.
+
+Hint Resolve ltA_trans.
+Hint Immediate ltA_eqA eqA_ltA.
+
+Notation InfA:=(lelistA ltA).
+Notation SortA:=(sort ltA).
+
+Lemma InfA_ltA :
+ forall l x y, ltA x y -> InfA y l -> InfA x l.
+Proof.
+ intro s; case s; constructor; inversion_clear H0.
+ eapply ltA_trans; eauto.
+Qed.
+ 
+Lemma InfA_eqA :
+ forall l x y, eqA x y -> InfA y l -> InfA x l.
+Proof.
+ intro s; case s; constructor; inversion_clear H0; eauto.
+Qed.
+Hint Immediate InfA_ltA InfA_eqA. 
+
+Lemma SortA_InfA_InA :
+ forall l x a, SortA l -> InfA a l -> InA x l -> ltA a x.
+Proof. 
+ simple induction l.
+ intros; inversion H1.
+ intros.
+ inversion_clear H0; inversion_clear H1; inversion_clear H2.
+ eapply ltA_eqA; eauto.
+ eauto.
+Qed.
+  
+Lemma In_InfA :
+ forall l x, (forall y, In y l -> ltA x y) -> InfA x l.
+Proof.
+ simple induction l; simpl in |- *; intros; constructor; auto.
+Qed.
+ 
+Lemma InA_InfA :
+ forall l x, (forall y, InA y l -> ltA x y) -> InfA x l.
+Proof.
+ simple induction l; simpl in |- *; intros; constructor; auto.
+Qed.
+
+(* In fact, this may be used as an alternative definition for InfA: *)
+
+Lemma InfA_alt : 
+ forall l x, SortA l -> (InfA x l <-> (forall y, InA y l -> ltA x y)).
+Proof. 
+split.
+intros; eapply SortA_InfA_InA; eauto.
+apply InA_InfA.
+Qed.
+
+Lemma SortA_NoDupA : forall l, SortA l -> NoDupA l.
+Proof.
+ simple induction l; auto.
+ intros x l' H H0.
+ inversion_clear H0.
+ constructor; auto.  
+ intro.
+ assert (ltA x x) by eapply SortA_InfA_InA; eauto.
+ elim (ltA_not_eqA H3); auto.
+Qed.
+
+Lemma NoDupA_app : forall l l', NoDupA l -> NoDupA l' -> 
+  (forall x, InA x l -> InA x l' -> False) -> 
+  NoDupA (l++l').
+Proof.
+induction l; simpl; auto; intros.
+inversion_clear H.
+constructor.
+rewrite InA_alt; intros (y,(H4,H5)).
+destruct (in_app_or _ _ _ H5).
+elim H2.
+rewrite InA_alt.
+exists y; auto.
+apply (H1 a).
+auto.
+rewrite InA_alt.
+exists y; auto.
+apply IHl; auto.
+intros.
+apply (H1 x); auto.
+Qed.
+
+
+Lemma NoDupA_rev : forall l, NoDupA l -> NoDupA (rev l).
+Proof.
+induction l.
+simpl; auto.
+simpl; intros.
+inversion_clear H.
+apply NoDupA_app; auto.
+constructor; auto.
+intro H2; inversion H2.
+intros x.
+rewrite InA_alt.
+intros (x1,(H2,H3)).
+inversion_clear 1.
+destruct H0.
+apply InA_eqA with x1; eauto.
+apply In_InA.
+rewrite In_rev; auto.
+inversion H4.
+Qed.
+
+
+Lemma InA_app : forall l1 l2 x,
+ InA x (l1 ++ l2) -> InA x l1 \/ InA x l2.
+Proof.
+ induction l1; simpl in *; intuition.
+ inversion_clear H; auto.
+ elim (IHl1 l2 x H0); auto.
+Qed.
+
+ Hint Constructors lelistA sort.
+
+Lemma InfA_app : forall l1 l2 a, InfA a l1 -> InfA a l2 -> InfA a (l1++l2).
+Proof.
+ induction l1; simpl; auto.
+ inversion_clear 1; auto.
+Qed.
+
+Lemma SortA_app :
+ forall l1 l2, SortA l1 -> SortA l2 ->
+ (forall x y, InA x l1 -> InA y l2 -> ltA x y) ->
+ SortA (l1 ++ l2).
+Proof.
+ induction l1; simpl in *; intuition.
+ inversion_clear H.
+ constructor; auto.
+ apply InfA_app; auto.
+ destruct l2; auto.
+Qed.
+
+Section Remove.
+
+Hypothesis eqA_dec : forall x y : A, {eqA x y}+{~(eqA x y)}.
+
+Fixpoint removeA (x : A) (l : list A){struct l} : list A :=
+  match l with
+    | nil => nil
+    | y::tl => if (eqA_dec x y) then removeA x tl else y::(removeA x tl)
+  end.
+
+Lemma removeA_filter : forall x l, 
+  removeA x l = filter (fun y => if eqA_dec x y then false else true) l.
+Proof.
+induction l; simpl; auto.
+destruct (eqA_dec x a); auto.
+rewrite IHl; auto.
+Qed.
+
+Lemma removeA_InA : forall l x y, InA y (removeA x l) <-> InA y l /\ ~eqA x y.
+Proof.
+induction l; simpl; auto.
+split.
+inversion_clear 1.
+destruct 1; inversion_clear H.
+intros.
+destruct (eqA_dec x a); simpl; auto.
+rewrite IHl; split; destruct 1; split; auto.
+inversion_clear H; auto.
+destruct H0; apply eqA_trans with a; auto.
+split.
+inversion_clear 1.
+split; auto.
+swap n.
+apply eqA_trans with y; auto.
+rewrite (IHl x y) in H0; destruct H0; auto.
+destruct 1; inversion_clear H; auto.
+constructor 2; rewrite IHl; auto.
+Qed.
+
+Lemma removeA_NoDupA :
+  forall s x, NoDupA s ->  NoDupA (removeA x s).
+Proof.
+simple induction s; simpl; intros.
+auto.
+inversion_clear H0.
+destruct (eqA_dec x a); simpl; auto. 
+constructor; auto.
+rewrite removeA_InA.
+intuition.
+Qed. 
+
+Lemma removeA_eqlistA : forall l l' x, 
+  ~InA x l -> eqlistA (x :: l) l' -> eqlistA l (removeA x l').
+Proof.  
+unfold eqlistA; intros. 
+rewrite removeA_InA.
+split; intros.
+rewrite <- H0; split; auto.
+swap H.
+apply InA_eqA with x0; auto.
+rewrite <- (H0 x0) in H1.
+destruct H1.
+inversion_clear H1; auto.
+elim H2; auto.
+Qed.
+
+End Remove.
+
+End Type_with_equality.
+
+Hint Constructors InA.
+Hint Constructors NoDupA. 
+Hint Constructors sort.
+Hint Constructors lelistA.
diff --git a/theories/Lists/Streams.v b/theories/Lists/Streams.v
index 3c433ba2..7bc6a09d 100755..100644
--- a/theories/Lists/Streams.v
+++ b/theories/Lists/Streams.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Streams.v,v 1.15.2.1 2004/07/16 19:31:05 herbelin Exp $ i*)
+(*i $Id: Streams.v 8642 2006-03-17 10:09:02Z notin $ i*)
 
 Set Implicit Arguments.
 
@@ -71,9 +71,8 @@ Qed.
 
 (** Extensional Equality between two streams  *)
 
-CoInductive EqSt : Stream -> Stream -> Prop :=
+CoInductive EqSt (s1 s2: Stream) : Prop :=
     eqst :
-      forall s1 s2:Stream,
         hd s1 = hd s2 -> EqSt (tl s1) (tl s2) -> EqSt s1 s2.
 
 (** A coinduction principle *)
@@ -140,12 +139,12 @@ Inductive Exists : Stream -> Prop :=
   | Further : forall x:Stream, ~ P x -> Exists (tl x) -> Exists x.
 i*)
 
-Inductive Exists : Stream -> Prop :=
-  | Here : forall x:Stream, P x -> Exists x
-  | Further : forall x:Stream, Exists (tl x) -> Exists x.
+Inductive Exists ( x: Stream ) : Prop :=
+  | Here : P x -> Exists x
+  | Further : Exists (tl x) -> Exists x.
 
-CoInductive ForAll : Stream -> Prop :=
-    HereAndFurther : forall x:Stream, P x -> ForAll (tl x) -> ForAll x.
+CoInductive ForAll (x: Stream) : Prop :=
+    HereAndFurther : P x -> ForAll (tl x) -> ForAll x.
 
 
 Section Co_Induction_ForAll.
diff --git a/theories/Lists/TheoryList.v b/theories/Lists/TheoryList.v
index fbeb97ce..19f97aec 100755..100644
--- a/theories/Lists/TheoryList.v
+++ b/theories/Lists/TheoryList.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: TheoryList.v,v 1.15.2.1 2004/07/16 19:31:06 herbelin Exp $ i*)
+(*i $Id: TheoryList.v 8642 2006-03-17 10:09:02Z notin $ i*)
 
 (** Some programs and results about lists following CAML Manual *)
 
diff --git a/theories/Lists/intro.tex b/theories/Lists/intro.tex
index 344bba59..c45f8803 100755
--- a/theories/Lists/intro.tex
+++ b/theories/Lists/intro.tex
@@ -4,21 +4,24 @@ This library includes the following files:
 
 \begin{itemize}
 
-\item {\tt List.v} THIS OLD LIBRARY IS HERE ONLY FOR COMPATIBILITY
-  WITH OLDER VERSIONS OF COQS. THE USER SHOULD USE POLYLIST INSTEAD.
-
-\item {\tt PolyList.v} contains definitions of (polymorphic) lists, 
+\item {\tt List.v} contains definitions of (polymorphic) lists, 
   functions on lists such as head, tail, map, append and prove some
   properties of these functions. Implicit arguments are used in this
-  library, so you should read the Referance Manual about implicit
+  library, so you should read the Reference Manual about implicit
   arguments before using it.
 
+\item {\tt ListSet.v} contains definitions and properties of finite
+  sets, implemented as lists.
+
 \item {\tt TheoryList.v} contains complementary results on lists. Here
-  a more theoric point of view is assumed : one extracts functions
+  a more theoretic point of view is assumed : one extracts functions
   from propositions, rather than defining functions and then prove them.
 
 \item {\tt Streams.v} defines the type of infinite lists (streams). It is a
   coinductive type. Basic facts are stated and proved. The streams are
   also polymorphic.
 
+\item {\tt MonoList.v} THIS OLD LIBRARY IS HERE ONLY FOR COMPATIBILITY
+  WITH OLDER VERSIONS OF COQ. THE USER SHOULD USE {\tt List.v} INSTEAD.
+
 \end{itemize}