Delete trailing whitespaces in all *.{v,ml*} files

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

7 files changed, 307 insertions, 307 deletions

diff --git a/theories/Lists/List.v b/theories/Lists/List.v
index 9add5f48d4..f2961635ec 100644
--- a/theories/Lists/List.v
+++ b/theories/Lists/List.v
@@ -42,7 +42,7 @@ Section Lists.
    match l with
      | nil => default
      | x :: _ => x
-   end. 
+   end.
 
   Definition tail (l:list) : list :=
     match l with
@@ -71,9 +71,9 @@ Section Lists.
       | 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 *)
@@ -101,7 +101,7 @@ Section Facts.
 
   (** Discrimination *)
   Theorem nil_cons : forall (x:A) (l:list A), nil <> x :: l.
-  Proof. 
+  Proof.
     intros; discriminate.
   Qed.
 
@@ -114,9 +114,9 @@ Section Facts.
     right; reflexivity.
     left; exists a; exists tl; reflexivity.
   Qed.
-    
+
   (** *** Head and tail *)
-  
+
   Theorem head_nil : head (@nil A) = None.
   Proof.
     simpl; reflexivity.
@@ -129,19 +129,19 @@ Section Facts.
 
 
   (************************)
-  (** *** Facts about [In] *) 
+  (** *** Facts about [In] *)
   (************************)
 
 
   (** Characterization of [In] *)
-  
+
   Theorem in_eq : forall (a:A) (l:list A), In a (a :: l).
-  Proof. 
+  Proof.
     simpl in |- *; auto.
   Qed.
-  
+
   Theorem in_cons : forall (a b:A) (l:list A), In b l -> In b (a :: l).
-  Proof. 
+  Proof.
     simpl in |- *; auto.
   Qed.
 
@@ -173,7 +173,7 @@ Section Facts.
     intro H; induction l as [| a0 l IHl].
     right; apply in_nil.
     destruct (H a0 a); simpl in |- *; auto.
-    destruct IHl; simpl in |- *; auto. 
+    destruct IHl; simpl in |- *; auto.
     right; unfold not in |- *; intros [Hc1| Hc2]; auto.
   Defined.
 
@@ -199,7 +199,7 @@ Section Facts.
   Qed.
 
   Theorem app_nil_r : forall l:list A, l ++ nil = l.
-  Proof. 
+  Proof.
     induction l; simpl; f_equal; auto.
   Qed.
 
@@ -211,23 +211,23 @@ Section Facts.
 
   (** [app] is associative *)
   Theorem app_assoc : forall l m n:list A, l ++ m ++ n = (l ++ m) ++ n.
-  Proof. 
+  Proof.
     intros l m n; induction l; simpl; f_equal; auto.
   Qed.
 
   Theorem app_assoc_reverse : forall l m n:list A, (l ++ m) ++ n = l ++ m ++ n.
-  Proof. 
+  Proof.
      auto using app_assoc.
   Qed.
   Hint Resolve app_assoc_reverse.
 
-  (** [app] commutes with [cons] *) 
+  (** [app] commutes with [cons] *)
   Theorem app_comm_cons : forall (x y:list A) (a:A), a :: (x ++ y) = (a :: x) ++ y.
   Proof.
     auto.
   Qed.
 
-  (** Facts deduced from the result of a concatenation *)  
+  (** Facts deduced from the result of a concatenation *)
 
   Theorem app_eq_nil : forall l l':list A, l ++ l' = nil -> l = nil /\ l' = nil.
   Proof.
@@ -261,7 +261,7 @@ Section Facts.
     forall (x y:list A) (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] ]; 
+      [ destruct y as [| a l] | destruct y as [| a l0] ];
       simpl in |- *; auto.
     intros a b H.
     injection H.
@@ -276,7 +276,7 @@ Section Facts.
     generalize (app_cons_not_nil _ _ _ H2); destruct 1.
     intros a0 b H.
     injection H; intros.
-    destruct (IHl l0 a0 b H0). 
+    destruct (IHl l0 a0 b H0).
     split; auto.
     rewrite <- H1; rewrite <- H2; reflexivity.
   Qed.
@@ -290,7 +290,7 @@ Section Facts.
   Qed.
 
   Lemma in_app_or : forall (l m:list A) (a:A), In a (l ++ m) -> In a l \/ In a m.
-  Proof. 
+  Proof.
     intros l m a.
     elim l; simpl in |- *; auto.
     intros a0 y H H0.
@@ -302,7 +302,7 @@ Section Facts.
   Qed.
 
   Lemma in_or_app : forall (l m:list A) (a:A), In a l \/ In a m -> In a (l ++ m).
-  Proof. 
+  Proof.
     intros l m a.
     elim l; simpl in |- *; intro H.
     now_show (In a m).
@@ -327,12 +327,12 @@ Section Facts.
   Proof.
     induction l; simpl; auto; injection 1; auto.
   Qed.
- 
+
   Lemma app_inv_tail:
     forall l l1 l2 : list A, l1 ++ l = l2 ++ l ->  l1 = l2.
   Proof.
     intros l l1 l2; revert l1 l2 l.
-    induction l1 as [ | x1 l1]; destruct l2 as [ | x2 l2]; 
+    induction l1 as [ | x1 l1]; destruct l2 as [ | x2 l2];
      simpl; auto; intros l H.
     absurd (length (x2 :: l2 ++ l) <= length l).
     simpl; rewrite app_length; auto with arith.
@@ -348,7 +348,7 @@ End Facts.
 Hint Resolve app_assoc app_assoc_reverse: datatypes v62.
 Hint Resolve app_comm_cons app_cons_not_nil: datatypes v62.
 Hint Immediate app_eq_nil: datatypes v62.
-Hint Resolve app_eq_unit app_inj_tail: datatypes v62. 
+Hint Resolve app_eq_unit app_inj_tail: datatypes v62.
 Hint Resolve in_eq in_cons in_inv in_nil in_app_or in_or_app: datatypes v62.
 
 
@@ -384,18 +384,18 @@ Section Elts.
   Lemma nth_in_or_default :
     forall (n:nat) (l:list A) (d:A), {In (nth n l d) l} + {nth n l d = d}.
   (* Realizer nth_ok. Program_all. *)
-  Proof. 
+  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.     
+    intro n1; elim (IHl n1); auto.
   Qed.
 
   Lemma nth_S_cons :
     forall (n:nat) (l:list A) (d a:A),
       In (nth n l d) l -> In (nth (S n) (a :: l) d) (a :: l).
-  Proof. 
+  Proof.
     simpl in |- *; auto.
   Qed.
 
@@ -436,7 +436,7 @@ Section Elts.
     apply IHl; auto with arith.
   Qed.
 
-  Lemma nth_indep : 
+  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.
@@ -444,7 +444,7 @@ Section Elts.
     destruct n; simpl; auto with arith.
   Qed.
 
-  Lemma app_nth1 : 
+  Lemma app_nth1 :
     forall l l' d n, n < length l -> nth n (l++l') d = nth n l d.
   Proof.
     induction l.
@@ -455,7 +455,7 @@ Section Elts.
     intros; rewrite IHl; auto with arith.
   Qed.
 
-  Lemma app_nth2 : 
+  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.
@@ -480,22 +480,22 @@ Section Elts.
   Section Remove.
 
     Hypothesis eq_dec : forall x y : A, {x = y}+{x <> y}.
-    
+
     Fixpoint remove (x : A) (l : list A){struct l} : list A :=
       match l with
 	| nil => nil
 	| y::tl => if (eq_dec x y) then remove x tl else y::(remove x tl)
       end.
-    
+
     Theorem remove_In : forall (l : list A) (x : A), ~ In x (remove x l).
     Proof.
       induction l as [|x l]; auto.
-      intro y; simpl; destruct (eq_dec y x) as [yeqx | yneqx]. 
+      intro y; simpl; destruct (eq_dec y x) as [yeqx | yneqx].
       apply IHl.
       unfold not; intro HF; simpl in HF; destruct HF; auto.
-      apply (IHl y); assumption. 
+      apply (IHl y); assumption.
     Qed.
-  
+
   End Remove.
 
 
@@ -503,26 +503,26 @@ Section Elts.
 (** ** Last element of a list *)
 (******************************)
 
-  (** [last l d] returns the last element of the list [l], 
+  (** [last l d] returns the last element of the list [l],
     or the default value [d] if [l] is empty. *)
 
-  Fixpoint last (l:list A) (d:A)  {struct l} : A := 
-  match l with 
-    | nil => d 
-    | a :: nil => a 
+  Fixpoint last (l:list A) (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 A) {struct l} : list A := 
-    match l with 
-      | nil =>  nil 
-      | a :: nil => nil 
+  Fixpoint removelast (l:list A) {struct l} : list A :=
+    match l with
+      | nil =>  nil
+      | a :: nil => nil
       | a :: l => a :: removelast l
     end.
-  
-  Lemma app_removelast_last : 
+
+  Lemma app_removelast_last :
     forall l d, l<>nil -> l = removelast l ++ (last l d :: nil).
   Proof.
     induction l.
@@ -531,10 +531,10 @@ Section Elts.
     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 : A | l = l'++a::nil}}. 
-  Proof. 
+
+  Lemma exists_last :
+    forall l, l<>nil -> { l' : (list A) & { a : A | l = l'++a::nil}}.
+  Proof.
     induction l.
     destruct 1; auto.
     intros _.
@@ -545,7 +545,7 @@ Section Elts.
     exists (a::l'); exists a'; auto.
   Qed.
 
-  Lemma removelast_app : 
+  Lemma removelast_app :
     forall l l', l' <> nil -> removelast (l++l') = l ++ removelast l'.
   Proof.
     induction l.
@@ -559,31 +559,31 @@ Section Elts.
     destruct (l++l'); [elim H0; auto|f_equal; auto].
   Qed.
 
-  
+
   (****************************************)
   (** ** Counting occurences of a element *)
   (****************************************)
 
   Hypotheses eqA_dec : forall x y : A, {x = y}+{x <> y}.
-  
+
   Fixpoint count_occ (l : list A) (x : A){struct l} : nat :=
-    match l with 
+    match l with
       | nil => 0
-      | y :: tl => 
-	let n := count_occ tl x in 
+      | y :: tl =>
+	let n := count_occ tl x in
 	  if eqA_dec y x then S n else n
     end.
-  
+
   (** Compatibility of count_occ with operations on list *)
   Theorem count_occ_In : forall (l : list A) (x : A), In x l <-> count_occ l x > 0.
   Proof.
     induction l as [|y l].
     simpl; intros; split; [destruct 1 | apply gt_irrefl].
     simpl. intro x; destruct (eqA_dec y x) as [Heq|Hneq].
-    rewrite Heq; intuition. 
+    rewrite Heq; intuition.
     pose (IHl x). intuition.
   Qed.
-  
+
   Theorem count_occ_inv_nil : forall (l : list A), (forall x:A, count_occ l x = 0) <-> l = nil.
   Proof.
     split.
@@ -600,7 +600,7 @@ Section Elts.
     (* Case <- *)
     intro H; rewrite H; simpl; reflexivity.
   Qed.
-  
+
   Lemma count_occ_nil : forall (x : A), count_occ nil x = 0.
   Proof.
     intro x; simpl; reflexivity.
@@ -611,11 +611,11 @@ Section Elts.
     intros l x y H; simpl.
     destruct (eqA_dec x y); [reflexivity | contradiction].
   Qed.
-  
+
   Lemma count_occ_cons_neq : forall (l : list A) (x y : A), x <> y -> count_occ (x::l) y = count_occ l y.
   Proof.
     intros l x y H; simpl.
-    destruct (eqA_dec x y); [contradiction | reflexivity]. 
+    destruct (eqA_dec x y); [contradiction | reflexivity].
   Qed.
 
 End Elts.
@@ -697,7 +697,7 @@ Section ListOps.
     elim (length l); simpl; auto.
   Qed.
 
-  Lemma rev_nth : forall l d n,  n < length l ->  
+  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.
@@ -720,11 +720,11 @@ Section ListOps.
   Qed.
 
 
-  (**  An alternative tail-recursive definition for reverse *) 
+  (**  An alternative tail-recursive definition for reverse *)
 
-  Fixpoint rev_append (l l': list A) {struct l} : list A := 
-    match l with 
-      | nil => l' 
+  Fixpoint rev_append (l l': list A) {struct l} : list A :=
+    match l with
+      | nil => l'
       | a::l => rev_append l (a::l')
     end.
 
@@ -750,11 +750,11 @@ Section ListOps.
 (*********************************************)
 (** Reverse Induction Principle on Lists  *)
 (*********************************************)
-  
+
   Section Reverse_Induction.
-    
+
     Unset Implicit Arguments.
-    
+
     Lemma rev_list_ind :
       forall P:list A-> Prop,
 	P nil ->
@@ -764,7 +764,7 @@ Section ListOps.
       induction l; auto.
     Qed.
     Set Implicit Arguments.
-    
+
     Theorem rev_ind :
       forall P:list A -> Prop,
 	P nil ->
@@ -775,13 +775,13 @@ Section ListOps.
       intros E; rewrite <- E.
       apply (rev_list_ind P).
       auto.
-      
+
       simpl in |- *.
       intros.
       apply (H0 a (rev l0)).
       auto.
     Qed.
-  
+
   End Reverse_Induction.
 
 
@@ -818,7 +818,7 @@ Section ListOps.
 
     Theorem Permutation_refl : forall l : list A, Permutation l l.
     Proof.
-      induction l; constructor. exact IHl. 
+      induction l; constructor. exact IHl.
     Qed.
 
     Theorem Permutation_sym : forall l l' : list A, Permutation l l' -> Permutation l' l.
@@ -838,7 +838,7 @@ Section ListOps.
 
     Theorem Permutation_in : forall (l l' : list A) (x : A), Permutation l l' -> In x l -> In x l'.
     Proof.
-      intros l l' x Hperm; induction Hperm; simpl; tauto. 
+      intros l l' x Hperm; induction Hperm; simpl; tauto.
     Qed.
 
     Lemma Permutation_app_tail : forall (l l' tl : list A), Permutation l l' -> Permutation (l++tl) (l'++tl).
@@ -863,7 +863,7 @@ Section ListOps.
 
     Theorem Permutation_app_swap : forall (l l' : list A), Permutation (l++l') (l'++l).
     Proof.
-      induction l as [|x l]. 
+      induction l as [|x l].
       simpl; intro l'; rewrite app_nil_r; trivial.
       induction l' as [|y l'].
       simpl; rewrite app_nil_r; trivial.
@@ -872,7 +872,7 @@ Section ListOps.
       apply Permutation_trans with (l' := y :: x :: l' ++ l); constructor.
       apply Permutation_trans with (l' := x :: l ++ l'); auto.
     Qed.
-  
+
     Theorem Permutation_cons_app : forall (l l1 l2:list A) a,
       Permutation l (l1 ++ l2) -> Permutation (a :: l) (l1 ++ a :: l2).
     Proof.
@@ -895,7 +895,7 @@ Section ListOps.
       apply trans_eq with (y:= (length l')); trivial.
     Qed.
 
-    Theorem Permutation_rev : forall (l : list A), Permutation l (rev l). 
+    Theorem Permutation_rev : forall (l : list A), Permutation l (rev l).
     Proof.
       induction l as [| x l]; simpl; trivial.
       apply Permutation_trans with (l' := (x::nil)++rev l).
@@ -903,7 +903,7 @@ Section ListOps.
       apply Permutation_app_swap.
     Qed.
 
-    Theorem Permutation_ind_bis : 
+    Theorem Permutation_ind_bis :
      forall P : list A -> list A -> Prop,
        P (@nil A) (@nil A) ->
        (forall x l l', Permutation l l' -> P l l' -> P (x :: l) (x :: l')) ->
@@ -922,14 +922,14 @@ Section ListOps.
     eauto.
     Qed.
 
-    Ltac break_list l x l' H := 
-     destruct l as [|x l']; simpl in *; 
+    Ltac break_list l x l' H :=
+     destruct l as [|x l']; simpl in *;
      injection H; intros; subst; clear H.
 
     Theorem Permutation_app_inv : forall (l1 l2 l3 l4:list A) a,
       Permutation (l1++a::l2) (l3++a::l4) -> Permutation (l1++l2) (l3 ++ l4).
     Proof.
-    set (P:=fun l l' =>  
+    set (P:=fun l l' =>
              forall a l1 l2 l3 l4, l=l1++a::l2 -> l'=l3++a::l4 -> Permutation (l1++l2) (l3++l4)).
     cut (forall l l', Permutation l l' -> P l l').
     intros; apply (H _ _ H0 a); auto.
@@ -951,10 +951,10 @@ Section ListOps.
     break_list l3' b l3'' H.
     auto.
     apply perm_trans with (c::l3''++b::l4); auto.
-    break_list l1' c l1'' H1. 
+    break_list l1' c l1'' H1.
     auto.
     apply perm_trans with (b::l1''++c::l2); auto.
-    break_list l3' d l3'' H; break_list l1' e l1'' H1. 
+    break_list l3' d l3'' H; break_list l1' e l1'' H1.
     auto.
     apply perm_trans with (e::a::l1''++l2); auto.
     apply perm_trans with (e::l1''++a::l2); auto.
@@ -974,28 +974,28 @@ Section ListOps.
     apply (H2 _ _ _ _ _ H6 H4).
     Qed.
 
-    Theorem Permutation_cons_inv : 
+    Theorem Permutation_cons_inv :
        forall l l' a, Permutation (a::l) (a::l') -> Permutation l l'.
     Proof.
-    intros; exact (Permutation_app_inv (@nil _) l (@nil _) l' a H). 
+    intros; exact (Permutation_app_inv (@nil _) l (@nil _) l' a H).
     Qed.
 
     Theorem Permutation_cons_app_inv :
        forall l l1 l2 a, Permutation (a :: l) (l1 ++ a :: l2) -> Permutation l (l1 ++ l2).
     Proof.
-    intros; exact (Permutation_app_inv (@nil _) l l1 l2 a H). 
+    intros; exact (Permutation_app_inv (@nil _) l l1 l2 a H).
     Qed.
-    
-    Theorem Permutation_app_inv_l : 
+
+    Theorem Permutation_app_inv_l :
         forall l l1 l2, Permutation (l ++ l1) (l ++ l2) -> Permutation l1 l2.
-    Proof.    
+    Proof.
     induction l; simpl; auto.
     intros.
     apply IHl.
     apply Permutation_cons_inv with a; auto.
     Qed.
 
-    Theorem Permutation_app_inv_r : 
+    Theorem Permutation_app_inv_r :
        forall l l1 l2, Permutation (l1 ++ l) (l2 ++ l) -> Permutation l1 l2.
     Proof.
     induction l.
@@ -1019,9 +1019,9 @@ Section ListOps.
   Proof.
     induction l as [| x l IHl]; destruct l' as [| y l'].
     left; trivial.
-    right; apply nil_cons. 
+    right; apply nil_cons.
     right; unfold not; intro HF; apply (nil_cons (sym_eq HF)).
-    destruct (eqA_dec x y) as [xeqy|xneqy]; destruct (IHl l') as [leql'|lneql']; 
+    destruct (eqA_dec x y) as [xeqy|xneqy]; destruct (IHl l') as [leql'|lneql'];
       try (right; unfold not; intro HF; injection HF; intros; contradiction).
     rewrite xeqy; rewrite leql'; left; trivial.
   Qed.
@@ -1041,21 +1041,21 @@ End ListOps.
 Section Map.
   Variables A B : Type.
   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.
-  
+
   Lemma in_map :
     forall (l:list A) (x:A), In x l -> In (f x) (map l).
-  Proof. 
+  Proof.
     induction l as [| a l IHl]; simpl in |- *;
       [ auto
 	| destruct 1; [ left; apply f_equal with (f := f); assumption | auto ] ].
   Qed.
-  
+
   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).
@@ -1066,7 +1066,7 @@ Section Map.
     induction l; simpl; auto.
   Qed.
 
-  Lemma map_nth : forall l d n, 
+  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.
@@ -1078,15 +1078,15 @@ Section Map.
     induction n; intros [ | ] ? Heq; simpl in *; inversion Heq; auto.
   Qed.
 
-  Lemma map_app : forall l l',  
+  Lemma map_app : forall l l',
     map (l++l') = (map l)++(map l').
-  Proof. 
+  Proof.
     induction l; simpl; auto.
     intros; rewrite IHl; auto.
   Qed.
-  
+
   Lemma map_rev : forall l, map (rev l) = rev (map l).
-  Proof. 
+  Proof.
     induction l; simpl; auto.
     rewrite map_app.
     rewrite IHl; auto.
@@ -1094,23 +1094,23 @@ Section Map.
 
   Hint Constructors Permutation.
 
-  Lemma Permutation_map : 
+  Lemma Permutation_map :
     forall l l', Permutation l l' -> Permutation (map l) (map l').
-  Proof. 
+  Proof.
   induction 1; simpl; auto; eauto.
   Qed.
 
   (** [flat_map] *)
 
-  Fixpoint flat_map (f:A -> list B) (l:list A) {struct l} : 
+  Fixpoint flat_map (f:A -> list B) (l:list A) {struct l} :
     list B :=
     match l with
       | nil => nil
       | cons x t => (f x)++(flat_map f t)
     end.
-  
+
   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). 
+    In y (flat_map f l) <-> exists x, In x l /\ In y (f x).
   Proof.
     induction l; simpl; split; intros.
     contradiction.
@@ -1126,7 +1126,7 @@ Section Map.
     exists x; auto.
   Qed.
 
-End Map. 
+End Map.
 
 Lemma map_id : forall (A :Type) (l : list A),
   map (fun x => x) l = l.
@@ -1134,14 +1134,14 @@ Proof.
   induction l; simpl; auto; rewrite IHl; auto.
 Qed.
 
-Lemma map_map : forall (A B C:Type)(f:A->B)(g:B->C) l, 
+Lemma map_map : forall (A B C:Type)(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 : 
+Lemma map_ext :
   forall (A B : Type)(f g:A->B), (forall a, f a = g a) -> forall l, map f l = map g l.
 Proof.
   induction l; simpl; auto.
@@ -1156,17 +1156,17 @@ Qed.
 Section Fold_Left_Recursor.
   Variables A B : Type.
   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), 
+
+  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. 
+    induction l.
     simpl; auto.
     intros.
     simpl.
@@ -1175,7 +1175,7 @@ Section Fold_Left_Recursor.
 
 End Fold_Left_Recursor.
 
-Lemma fold_left_length : 
+Lemma fold_left_length :
   forall (A:Type)(l:list A), fold_left (fun x _ => S x) l 0 = length l.
 Proof.
   intro A.
@@ -1195,7 +1195,7 @@ Section Fold_Right_Recursor.
   Variables A B : Type.
   Variable f : B -> A -> A.
   Variable a0 : A.
-  
+
   Fixpoint fold_right (l:list B) : A :=
     match l with
       | nil => a0
@@ -1204,7 +1204,7 @@ Section Fold_Right_Recursor.
 
 End Fold_Right_Recursor.
 
-  Lemma fold_right_app : forall (A B:Type)(f:A->B->B) l l' i, 
+  Lemma fold_right_app : forall (A B:Type)(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.
@@ -1213,7 +1213,7 @@ End Fold_Right_Recursor.
     f_equal; auto.
   Qed.
 
-  Lemma fold_left_rev_right : forall (A B:Type)(f:A->B->B) l i, 
+  Lemma fold_left_rev_right : forall (A B:Type)(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.
@@ -1264,20 +1264,20 @@ End Fold_Right_Recursor.
   (** ** Boolean operations over lists *)
   (*************************************)
 
-  Section Bool. 
+  Section Bool.
     Variable A : Type.
     Variable f : A -> bool.
 
-  (** find whether a boolean function can be satisfied by an 
+  (** find whether a boolean function can be satisfied by an
        elements of the list. *)
 
-    Fixpoint existsb (l:list A) {struct l}: bool := 
-      match l with 
+    Fixpoint existsb (l:list A) {struct l}: bool :=
+      match l with
 	| nil => false
 	| a::l => f a || existsb l
       end.
 
-    Lemma existsb_exists : 
+    Lemma existsb_exists :
       forall l, existsb l = true <-> exists x, In x l /\ f x = true.
     Proof.
       induction l; simpl; intuition.
@@ -1296,11 +1296,11 @@ End Fold_Right_Recursor.
       inversion 1.
       simpl; intros.
       destruct (orb_false_elim _ _ H0); clear H0; auto.
-      destruct n ; auto. 
+      destruct n ; auto.
       rewrite IHl; auto with arith.
     Qed.
 
-    Lemma existsb_app : forall l1 l2, 
+    Lemma existsb_app : forall l1 l2,
       existsb (l1++l2) = existsb l1 || existsb l2.
     Proof.
       induction l1; intros l2; simpl.
@@ -1308,16 +1308,16 @@ End Fold_Right_Recursor.
       case (f a); simpl; solve[auto].
     Qed.
 
-  (** find whether a boolean function is satisfied by 
+  (** find whether a boolean function is satisfied by
     all the elements of a list. *)
 
-    Fixpoint forallb (l:list A) {struct l} : bool := 
-      match l with 
+    Fixpoint forallb (l:list A) {struct l} : bool :=
+      match l with
 	| nil => true
 	| a::l => f a && forallb l
       end.
 
-    Lemma forallb_forall : 
+    Lemma forallb_forall :
       forall l, forallb l = true <-> (forall x, In x l -> f x = true).
     Proof.
       induction l; simpl; intuition.
@@ -1326,7 +1326,7 @@ End Fold_Right_Recursor.
       destruct (andb_prop _ _ H1); auto.
       assert (forallb l = true).
       apply H0; intuition.
-      rewrite H1; auto. 
+      rewrite H1; auto.
     Qed.
 
     Lemma forallb_app :
@@ -1338,8 +1338,8 @@ End Fold_Right_Recursor.
     Qed.
   (** [filter] *)
 
-    Fixpoint filter (l:list A) : list A := 
-      match l with 
+    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.
@@ -1362,10 +1362,10 @@ End Fold_Right_Recursor.
 
   (** [partition] *)
 
-    Fixpoint partition (l:list A) {struct l} : list A * list A := 
+    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 
+	| x :: tl => let (g,d) := partition tl in
 	  if f x then (x::g,d) else (g,x::d)
       end.
 
@@ -1380,7 +1380,7 @@ End Fold_Right_Recursor.
 
   Section ListPairs.
     Variables A B : Type.
-    
+
   (** [split] derives two lists from a list of pairs *)
 
     Fixpoint split  (l:list (A*B)) { struct l }: list A * list B :=
@@ -1389,8 +1389,8 @@ End Fold_Right_Recursor.
 	| (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)). 
+    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 *.
@@ -1399,8 +1399,8 @@ End Fold_Right_Recursor.
       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)). 
+    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 *.
@@ -1409,7 +1409,7 @@ End Fold_Right_Recursor.
       right; apply (IHl (a0,b) H).
     Qed.
 
-    Lemma split_nth : forall (l:list (A*B))(n:nat)(d:A*B), 
+    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.
@@ -1421,21 +1421,21 @@ End Fold_Right_Recursor.
     Qed.
 
     Lemma split_length_l : forall (l:list (A*B)),
-      length (fst (split l)) = length l. 
+      length (fst (split l)) = length l.
     Proof.
       induction l; simpl; auto.
       destruct a; destruct (split l); simpl; auto.
     Qed.
 
     Lemma split_length_r : forall (l:list (A*B)),
-      length (snd (split l)) = length l. 
+      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. 
+  (** [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) :=
@@ -1444,17 +1444,17 @@ End Fold_Right_Recursor.
 	| _, _ => nil
       end.
 
-    Lemma split_combine : forall (l: list (A*B)), 
+    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 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' -> 
+    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.
@@ -1462,19 +1462,19 @@ End Fold_Right_Recursor.
       rewrite IHl; auto.
     Qed.
 
-    Lemma in_combine_l : forall (l:list A)(l':list B)(x:A)(y:B), 
+    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. 
+      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), 
+    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.
@@ -1485,7 +1485,7 @@ End Fold_Right_Recursor.
       right; apply IHl with x; auto.
     Qed.
 
-    Lemma combine_length : forall (l:list A)(l':list B), 
+    Lemma combine_length : forall (l:list A)(l':list B),
       length (combine l l') = min (length l) (length l').
     Proof.
       induction l.
@@ -1493,8 +1493,8 @@ End Fold_Right_Recursor.
       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' -> 
+    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.
@@ -1503,7 +1503,7 @@ End Fold_Right_Recursor.
     Qed.
 
   (** [list_prod] has the same signature as [combine], but unlike
-     [combine], it adds every possible pairs, not only those at the 
+     [combine], it adds every possible pairs, not only those at the
      same position. *)
 
     Fixpoint list_prod (l:list A) (l':list B) {struct l} :
@@ -1516,7 +1516,7 @@ End Fold_Right_Recursor.
     Lemma in_prod_aux :
       forall (x:A) (y:B) (l:list B),
 	In y l -> In (x, y) (map (fun y0:B => (x, y0)) l).
-    Proof. 
+    Proof.
       induction l;
 	[ simpl in |- *; auto
 	  | simpl in |- *; destruct 1 as [H1| ];
@@ -1526,15 +1526,15 @@ End Fold_Right_Recursor.
     Lemma in_prod :
       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. 
+    Proof.
       induction l;
 	[ simpl in |- *; tauto
 	  | simpl in |- *; intros; apply in_or_app; destruct H;
 	    [ 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), 
+    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 ].
@@ -1545,9 +1545,9 @@ End Fold_Right_Recursor.
       destruct (H1 H0) as (z,(H2,H3)); clear H0 H1.
       injection H2; clear H2; intros; subst; intuition.
       intuition.
-    Qed. 
+    Qed.
 
-    Lemma prod_length : forall (l:list A)(l':list B), 
+    Lemma prod_length : forall (l:list A)(l':list B),
       length (list_prod l l') = (length l) * (length l').
     Proof.
       induction l; simpl; auto.
@@ -1581,34 +1581,34 @@ Section length_order.
   Variables l m n : list A.
 
   Lemma lel_refl : lel l l.
-  Proof. 
+  Proof.
     unfold lel in |- *; auto with arith.
   Qed.
 
   Lemma lel_trans : lel l m -> lel m n -> lel l n.
-  Proof. 
+  Proof.
     unfold lel in |- *; intros.
     now_show (length l <= length n).
     apply le_trans with (length m); auto with arith.
   Qed.
 
   Lemma lel_cons_cons : lel l m -> lel (a :: l) (b :: m).
-  Proof. 
+  Proof.
     unfold lel in |- *; simpl in |- *; auto with arith.
   Qed.
 
   Lemma lel_cons : lel l m -> lel l (b :: m).
-  Proof. 
+  Proof.
     unfold lel in |- *; simpl in |- *; auto with arith.
   Qed.
 
   Lemma lel_tail : lel (a :: l) (b :: m) -> lel l m.
-  Proof. 
+  Proof.
     unfold lel in |- *; simpl in |- *; auto with arith.
   Qed.
 
   Lemma lel_nil : forall l':list A, lel l' nil -> nil = l'.
-  Proof. 
+  Proof.
     intro l'; elim l'; auto with arith.
     intros a' y H H0.
     now_show (nil = a' :: y).
@@ -1630,39 +1630,39 @@ Section SetIncl.
 
   Definition incl (l m:list A) := forall a:A, In a l -> In a m.
   Hint Unfold incl.
-  
+
   Lemma incl_refl : forall l:list A, incl l l.
-  Proof. 
+  Proof.
     auto.
   Qed.
   Hint Resolve incl_refl.
-  
+
   Lemma incl_tl : forall (a:A) (l m:list A), incl l m -> incl l (a :: m).
-  Proof. 
+  Proof.
     auto with datatypes.
   Qed.
   Hint Immediate incl_tl.
 
   Lemma incl_tran : forall l m n:list A, incl l m -> incl m n -> incl l n.
-  Proof. 
+  Proof.
     auto.
   Qed.
-  
+
   Lemma incl_appl : forall l m n:list A, incl l n -> incl l (n ++ m).
-  Proof. 
+  Proof.
     auto with datatypes.
   Qed.
   Hint Immediate incl_appl.
-  
+
   Lemma incl_appr : forall l m n:list A, incl l n -> incl l (m ++ n).
-  Proof. 
+  Proof.
     auto with datatypes.
   Qed.
   Hint Immediate incl_appr.
-  
+
   Lemma incl_cons :
     forall (a:A) (l m:list A), In a m -> incl l m -> incl (a :: l) m.
-  Proof. 
+  Proof.
     unfold incl in |- *; simpl in |- *; intros a l m H H0 a0 H1.
     now_show (In a0 m).
     elim H1.
@@ -1674,15 +1674,15 @@ Section SetIncl.
     auto.
   Qed.
   Hint Resolve incl_cons.
-  
+
   Lemma incl_app : forall l m n:list A, incl l n -> incl m n -> incl (l ++ m) n.
-  Proof. 
+  Proof.
     unfold incl in |- *; simpl in |- *; intros l m n H H0 a H1.
     now_show (In a n).
     elim (in_app_or _ _ _ H1); auto.
   Qed.
   Hint Resolve incl_app.
-  
+
 End SetIncl.
 
 Hint Resolve incl_refl incl_tl incl_tran incl_appl incl_appr incl_cons
@@ -1697,24 +1697,24 @@ Section Cutting.
 
   Variable A : Type.
 
-  Fixpoint firstn (n:nat)(l:list A) {struct n} : list A := 
-    match n with 
-      | 0 => nil 
-      | S n => match l with  
-		 | nil => nil 
+  Fixpoint firstn (n:nat)(l:list A) {struct n} : list A :=
+    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 A) { struct n } : list A := 
-    match n with 
-      | 0 => l 
-      | S n => match l with 
-		 | nil => nil 
+
+  Fixpoint skipn (n:nat)(l:list A) { struct n } : list A :=
+    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.
@@ -1728,7 +1728,7 @@ Section Cutting.
     induction n; destruct l; simpl; auto.
   Qed.
 
-   Lemma removelast_firstn : forall n l, n < length l -> 
+   Lemma removelast_firstn : forall n l, n < length l ->
      removelast (firstn (S n) l) = firstn n l.
    Proof.
      induction n; destruct l.
@@ -1741,13 +1741,13 @@ Section Cutting.
      change (firstn (S n) (a::l)) with (a::firstn n l).
      rewrite removelast_app.
      rewrite IHn; auto with arith.
-     
+
      clear IHn; destruct l; simpl in *; try discriminate.
      inversion_clear H.
      inversion_clear H0.
    Qed.
 
-   Lemma firstn_removelast : forall n l, n < length l -> 
+   Lemma firstn_removelast : forall n l, n < length l ->
      firstn n (removelast l) = firstn n l.
    Proof.
      induction n; destruct l.
@@ -1772,10 +1772,10 @@ End Cutting.
 Section ReDun.
 
   Variable A : Type.
-  
-  Inductive NoDup : list A -> Prop := 
-    | NoDup_nil : NoDup nil 
-    | NoDup_cons : forall x l, ~ In x l -> NoDup l -> NoDup (x::l). 
+
+  Inductive NoDup : list A -> Prop :=
+    | NoDup_nil : NoDup nil
+    | NoDup_cons : forall x l, ~ In x l -> NoDup l -> NoDup (x::l).
 
   Lemma NoDup_remove_1 : forall l l' a, NoDup (l++a::l') -> NoDup (l++l').
   Proof.
@@ -1800,10 +1800,10 @@ Section ReDun.
   destruct (IHl _ _ H1); auto.
   Qed.
 
-  Lemma NoDup_Permutation : forall l l', 
+  Lemma NoDup_Permutation : forall l l',
     NoDup l -> NoDup l' -> (forall x, In x l <-> In x l') -> Permutation l l'.
   Proof.
-  induction l. 
+  induction l.
   destruct l'; simpl; intros.
   apply perm_nil.
   destruct (H1 a) as (_,H2); destruct H2; auto.
@@ -1823,7 +1823,7 @@ Section ReDun.
   subst x; destruct H2; auto.
   assert (In x (l'1++a::l'2)).
     apply in_or_app; destruct (in_app_or _ _ _ H); simpl; auto.
-  destruct (H1 x) as (_,H5); destruct H5; auto. 
+  destruct (H1 x) as (_,H5); destruct H5; auto.
   subst x.
   destruct (NoDup_remove_2 _ _ _ H0 H).
   Qed.
@@ -1837,21 +1837,21 @@ End ReDun.
 
 Section NatSeq.
 
-  (** [seq] computes the sequence of [len] contiguous integers 
+  (** [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 
+
+  Fixpoint seq (start len:nat) {struct len} : list nat :=
+    match len with
       | 0 => nil
       | S len => start :: seq (S start) len
-    end. 
-  
+    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, 
+
+  Lemma seq_nth : forall len start n d,
     n < len -> nth n (seq start len) d = start+n.
   Proof.
     induction len; intros.
@@ -1864,7 +1864,7 @@ Section NatSeq.
 
   Lemma seq_shift : forall len start,
     map S (seq start len) = seq (S start) len.
-  Proof. 
+  Proof.
     induction len; simpl; auto.
     intros.
     rewrite IHlen.
diff --git a/theories/Lists/ListSet.v b/theories/Lists/ListSet.v
index 77caa9c22b..d8a8183f36 100644
--- a/theories/Lists/ListSet.v
+++ b/theories/Lists/ListSet.v
@@ -47,7 +47,7 @@ Section first_definitions.
         | right _ => set_mem a x1
         end
     end.
- 
+
   (** If [a] belongs to [x], removes [a] from [x]. If not, does nothing *)
   Fixpoint set_remove (a:A) (x:set) {struct x} : set :=
     match x with
@@ -72,7 +72,7 @@ Section first_definitions.
     | nil => x
     | a1 :: y1 => set_add a1 (set_union x y1)
     end.
-        
+
   (** returns the set of all els of [x] that does not belong to [y] *)
   Fixpoint set_diff (x y:set) {struct x} : set :=
     match x with
@@ -80,7 +80,7 @@ Section first_definitions.
     | a1 :: x1 =>
         if set_mem a1 y then set_diff x1 y else set_add a1 (set_diff x1 y)
     end.
-   
+
 
   Definition set_In : A -> set -> Prop := In (A:=A).
 
@@ -123,7 +123,7 @@ Section first_definitions.
     case H3; auto.
   Qed.
 
- 
+
   Lemma set_mem_correct1 :
    forall (a:A) (x:set), set_mem a x = true -> set_In a x.
   Proof.
@@ -191,11 +191,11 @@ Section first_definitions.
 
   Lemma set_add_intro :
    forall (a b:A) (x:set), a = b \/ set_In a x -> set_In a (set_add b x).
-  
+
   Proof.
     intros a b x [H1| H2]; auto with datatypes.
   Qed.
- 
+
   Lemma set_add_elim :
    forall (a b:A) (x:set), set_In a (set_add b x) -> a = b \/ set_In a x.
 
@@ -225,7 +225,7 @@ Section first_definitions.
     simple induction x; simpl in |- *.
     discriminate.
     intros; elim (Aeq_dec a a0); intros; discriminate.
-  Qed.   
+  Qed.
 
 
   Lemma set_union_intro1 :
@@ -289,7 +289,7 @@ Section first_definitions.
     elim (set_mem a y); simpl in |- *; intros.
     auto with datatypes.
     absurd (set_In a y); auto with datatypes.
-    elim (set_mem a0 y); [ right; auto with datatypes | auto with datatypes ].     
+    elim (set_mem a0 y); [ right; auto with datatypes | auto with datatypes ].
   Qed.
 
   Lemma set_inter_elim1 :
@@ -324,7 +324,7 @@ Section first_definitions.
      set_In a (set_inter x y) -> set_In a x /\ set_In a y.
   Proof.
     eauto with datatypes.
-  Qed. 
+  Qed.
 
   Lemma set_diff_intro :
    forall (a:A) (x y:set),
@@ -354,7 +354,7 @@ Section first_definitions.
    forall (a:A) (x y:set), set_In a (set_diff x y) -> ~ set_In a y.
   intros a x y; elim x; simpl in |- *.
   intros; contradiction.
-  intros a0 l Hrec. 
+  intros a0 l Hrec.
   apply set_mem_ind2; auto.
   intros H1 H2; case (set_add_elim _ _ _ H2); intros; auto.
   rewrite H; trivial.
@@ -387,10 +387,10 @@ Section other_definitions.
   Definition set_fold_left : (B -> A -> B) -> set A -> B -> B :=
     fold_left (A:=B) (B:=A).
 
-  Definition set_fold_right (f:A -> B -> B) (x:set A) 
+  Definition set_fold_right (f:A -> B -> B) (x:set A)
     (b:B) : B := fold_right f b x.
 
- 
+
 End other_definitions.
 
 Unset Implicit Arguments.
diff --git a/theories/Lists/ListTactics.v b/theories/Lists/ListTactics.v
index 2da70c4673..0a21a9e277 100644
--- a/theories/Lists/ListTactics.v
+++ b/theories/Lists/ListTactics.v
@@ -22,10 +22,10 @@ Ltac list_fold_right fcons fnil l :=
 Ltac lazy_list_fold_right fcons fnil l :=
   let f :=
     match l with
-    | ?x :: ?tl => 
+    | ?x :: ?tl =>
          fun _ =>
          fcons x ltac:(fun _ => lazy_list_fold_right fcons fnil tl)
-    | nil => fun _ => fnil() 
+    | nil => fun _ => fnil()
     end in
   f().
 
@@ -75,7 +75,7 @@ Ltac check_is_list t :=
 
 Ltac check_fv l :=
   check_is_list l;
-  match type of l with 
+  match type of l with
   | list _ => idtac
   | _      => fail 100 "anomaly: built an ill-typed list"
   end.
diff --git a/theories/Lists/SetoidList.v b/theories/Lists/SetoidList.v
index f55043d370..20af2878b2 100644
--- a/theories/Lists/SetoidList.v
+++ b/theories/Lists/SetoidList.v
@@ -14,15 +14,15 @@ Require Export Setoid.
 Set Implicit Arguments.
 Unset Strict Implicit.
 
-(** * Logical relations over lists with respect to a setoid equality 
-      or ordering. *) 
+(** * Logical relations over lists with respect to a setoid equality
+      or ordering. *)
 
-(** This can be seen as a complement of predicate [lelistA] and [sort] 
+(** This can be seen as a complement of predicate [lelistA] and [sort]
     found in [Sorting]. *)
 
 Section Type_with_equality.
 Variable A : Type.
-Variable eqA : A -> A -> Prop. 
+Variable eqA : A -> A -> Prop.
 
 (** Being in a list modulo an equality relation over type [A]. *)
 
@@ -47,7 +47,7 @@ Qed.
 (** An alternative definition of [InA]. *)
 
 Lemma InA_alt : forall x l, InA x l <-> exists y, eqA x y /\ In y l.
-Proof. 
+Proof.
  induction l; intuition.
  inversion H.
  firstorder.
@@ -98,10 +98,10 @@ 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. 
+Proof.
  intros s x y.
  do 2 rewrite InA_alt.
- intros H (z,(U,V)).  
+ intros H (z,(U,V)).
  exists z; split; eauto.
 Qed.
 Hint Immediate InA_eqA.
@@ -109,12 +109,12 @@ 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.  
+ subst; auto.
 Qed.
 Hint Resolve In_InA.
 
-Lemma InA_split : forall l x, InA x l -> 
- exists l1, exists y, exists l2, 
+Lemma InA_split : forall l x, InA x l ->
+ exists l1, exists y, exists l2,
  eqA x y /\ l = l1++y::l2.
 Proof.
 induction l; inversion_clear 1.
@@ -144,7 +144,7 @@ Proof.
  apply in_or_app; auto.
 Qed.
 
-Lemma InA_rev : forall p m, 
+Lemma InA_rev : forall p m,
  InA p (rev m) <-> InA p m.
 Proof.
  intros; do 2 rewrite InA_alt.
@@ -173,20 +173,20 @@ Hint Constructors lelistA sort.
 Lemma InfA_ltA :
  forall l x y, ltA x y -> InfA y l -> InfA x l.
 Proof.
- destruct l; constructor; inversion_clear H0; 
+ destruct l; 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. 
+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. 
+Proof.
  simple induction l.
  intros; inversion H1.
  intros.
@@ -194,13 +194,13 @@ Proof.
  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.
@@ -209,9 +209,9 @@ Qed.
 
 (* In fact, this may be used as an alternative definition for InfA: *)
 
-Lemma InfA_alt : 
+Lemma InfA_alt :
  forall l x, SortA l -> (InfA x l <-> (forall y, InA y l -> ltA x y)).
-Proof. 
+Proof.
 split.
 intros; eapply SortA_InfA_InA; eauto.
 apply InA_InfA.
@@ -242,14 +242,14 @@ Proof.
  simple induction l; auto.
  intros x l' H H0.
  inversion_clear H0.
- constructor; auto.  
+ 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) -> 
+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.
@@ -325,14 +325,14 @@ Proof.
 induction 1; auto; simpl; congruence.
 Qed.
 
-Lemma eqlistA_app : forall l1 l1' l2 l2', 
+Lemma eqlistA_app : forall l1 l1' l2 l2',
    eqlistA l1 l1' -> eqlistA l2 l2' -> eqlistA (l1++l2) (l1'++l2').
 Proof.
 intros l1 l1' l2 l2' H; revert l2 l2'; induction H; simpl; auto.
 Qed.
 
-Lemma eqlistA_rev_app : forall l1 l1', 
-   eqlistA l1 l1' -> forall l2 l2', eqlistA l2 l2' -> 
+Lemma eqlistA_rev_app : forall l1 l1',
+   eqlistA l1 l1' -> forall l2 l2', eqlistA l2 l2' ->
    eqlistA ((rev l1)++l2) ((rev l1')++l2').
 Proof.
 induction 1; auto.
@@ -340,7 +340,7 @@ simpl; intros.
 do 2 rewrite app_ass; simpl; auto.
 Qed.
 
-Lemma eqlistA_rev : forall l1 l1', 
+Lemma eqlistA_rev : forall l1 l1',
    eqlistA l1 l1' -> eqlistA (rev l1) (rev l1').
 Proof.
 intros.
@@ -349,12 +349,12 @@ rewrite (app_nil_end (rev l1')).
 apply eqlistA_rev_app; auto.
 Qed.
 
-Lemma SortA_equivlistA_eqlistA : forall l l', 
+Lemma SortA_equivlistA_eqlistA : forall l l',
    SortA l -> SortA l' -> equivlistA l l' -> eqlistA l l'.
 Proof.
 induction l; destruct l'; simpl; intros; auto.
-destruct (H1 a); assert (H4 : InA a nil) by auto; inversion H4.  
-destruct (H1 a); assert (H4 : InA a nil) by auto; inversion H4.  
+destruct (H1 a); assert (H4 : InA a nil) by auto; inversion H4.
+destruct (H1 a); assert (H4 : InA a nil) by auto; inversion H4.
 inversion_clear H; inversion_clear H0.
 assert (forall y, InA y l -> ltA a y).
 intros; eapply SortA_InfA_InA with (l:=l); eauto.
@@ -374,10 +374,10 @@ constructor; auto.
 apply IHl; auto.
 split; intros.
 destruct (H1 x).
-assert (H8 : InA x (a0::l')) by auto; inversion_clear H8; auto. 
+assert (H8 : InA x (a0::l')) by auto; inversion_clear H8; auto.
 elim (@ltA_not_eqA a x); eauto.
 destruct (H1 x).
-assert (H8 : InA x (a::l)) by auto; inversion_clear H8; auto. 
+assert (H8 : InA x (a::l)) by auto; inversion_clear H8; auto.
 elim (@ltA_not_eqA a0 x); eauto.
 Qed.
 
@@ -399,7 +399,7 @@ rewrite filter_In in H; destruct H.
 eapply SortA_InfA_InA; eauto.
 Qed.
 
-Lemma filter_InA : forall f, (compat_bool f) -> 
+Lemma filter_InA : forall f, (compat_bool f) ->
  forall l x, InA x (List.filter f l) <-> InA x l /\ f x = true.
 Proof.
 intros; do 2 rewrite InA_alt; intuition.
@@ -410,8 +410,8 @@ destruct H1 as (y,(H0,H1)); exists y; rewrite filter_In; intuition.
   rewrite <- (H _ _ H0); auto.
 Qed.
 
-Lemma filter_split : 
- forall f, (forall x y, f x = true -> f y = false -> ltA x y) -> 
+Lemma filter_split :
+ forall f, (forall x y, f x = true -> f y = false -> ltA x y) ->
  forall l, SortA l -> l = filter f l ++ filter (fun x=>negb (f x)) l.
 Proof.
 induction l; simpl; intros; auto.
@@ -443,7 +443,7 @@ Definition compat_op (f : A -> B -> B) :=
 
 (** Two-argument functions that allow to reorder their arguments. *)
 Definition transpose (f : A -> B -> B) :=
-  forall (x y : A) (z : B), eqB (f x (f y z)) (f y (f x z)). 
+  forall (x y : A) (z : B), eqB (f x (f y z)) (f y (f x z)).
 
 (** A version of transpose with restriction on where it should hold *)
 Definition transpose_restr (R : A -> A -> Prop)(f : A -> B -> B) :=
@@ -454,16 +454,16 @@ Variable f:A->B->B.
 Variable i:B.
 Variable Comp:compat_op f.
 
-Lemma fold_right_eqlistA : 
-   forall s s', eqlistA s s' -> 
+Lemma fold_right_eqlistA :
+   forall s s', eqlistA s s' ->
    eqB (fold_right f i s) (fold_right f i s').
 Proof.
 induction 1; simpl; auto.
 reflexivity.
 Qed.
 
-Lemma equivlistA_NoDupA_split : forall l l1 l2 x y, eqA x y -> 
- NoDupA (x::l) -> NoDupA (l1++y::l2) -> 
+Lemma equivlistA_NoDupA_split : forall l l1 l2 x y, eqA x y ->
+ NoDupA (x::l) -> NoDupA (l1++y::l2) ->
  equivlistA (x::l) (l1++y::l2) -> equivlistA l (l1++l2).
 Proof.
  intros; intro a.
@@ -687,7 +687,7 @@ destruct (eqA_dec x a).
 left; auto.
 destruct IHl.
 left; auto.
-right; red; inversion_clear 1; contradiction. 
+right; red; inversion_clear 1; contradiction.
 Qed.
 
 Fixpoint removeA (x : A) (l : list A){struct l} : list A :=
@@ -731,16 +731,16 @@ Proof.
 simple induction s; simpl; intros.
 auto.
 inversion_clear H0.
-destruct (eqA_dec x a); simpl; auto. 
+destruct (eqA_dec x a); simpl; auto.
 constructor; auto.
 rewrite removeA_InA.
 intuition.
-Qed. 
+Qed.
 
-Lemma removeA_equivlistA : forall l l' x, 
+Lemma removeA_equivlistA : forall l l' x,
   ~InA x l -> equivlistA (x :: l) l' -> equivlistA l (removeA x l').
-Proof.  
-unfold equivlistA; intros. 
+Proof.
+unfold equivlistA; intros.
 rewrite removeA_InA.
 split; intros.
 rewrite <- H0; split; auto.
@@ -761,22 +761,22 @@ End Type_with_equality.
 Hint Unfold compat_bool compat_nat compat_P.
 Hint Constructors InA NoDupA sort lelistA eqlistA.
 
-Section Find. 
-Variable A B : Type. 
-Variable eqA : A -> A -> Prop. 
+Section Find.
+Variable A B : Type.
+Variable eqA : A -> A -> Prop.
 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.
 Hypothesis eqA_dec : forall x y : A, {eqA x y}+{~(eqA x y)}.
 
-Fixpoint findA (f : A -> bool) (l:list (A*B)) : option B := 
- match l with  
-  | nil => None 
+Fixpoint findA (f : A -> bool) (l:list (A*B)) : option B :=
+ match l with
+  | nil => None
   | (a,b)::l => if f a then Some b else findA f l
  end.
 
-Lemma findA_NoDupA : 
- forall l a b, 
- NoDupA (fun p p' => eqA (fst p) (fst p')) l -> 
+Lemma findA_NoDupA :
+ forall l a b,
+ NoDupA (fun p p' => eqA (fst p) (fst p')) l ->
  (InA (fun p p' => eqA (fst p) (fst p') /\ snd p = snd p') (a,b) l <->
   findA (fun a' => if eqA_dec a a' then true else false) l = Some b).
 Proof.
@@ -808,4 +808,4 @@ constructor 2.
 rewrite IHl; auto.
 Qed.
 
-End Find. 
+End Find.
diff --git a/theories/Lists/StreamMemo.v b/theories/Lists/StreamMemo.v
index bdbe0ecccd..e8b9358413 100644
--- a/theories/Lists/StreamMemo.v
+++ b/theories/Lists/StreamMemo.v
@@ -11,8 +11,8 @@ Require Import Streams.
 
 (** * Memoization *)
 
-(** Successive outputs of a given function [f] are stored in 
-    a stream in order to avoid duplicated computations. *) 
+(** Successive outputs of a given function [f] are stored in
+    a stream in order to avoid duplicated computations. *)
 
 Section MemoFunction.
 
@@ -24,8 +24,8 @@ CoFixpoint memo_make (n:nat) : Stream A := Cons (f n) (memo_make (S n)).
 Definition memo_list := memo_make 0.
 
 Fixpoint memo_get (n:nat) (l:Stream A) : A :=
-  match n with 
-    | O => hd l 
+  match n with
+    | O => hd l
     | S n1 => memo_get n1 (tl l)
   end.
 
@@ -49,7 +49,7 @@ Variable g: A -> A.
 Hypothesis Hg_correct: forall n, f (S n) = g (f n).
 
 CoFixpoint imemo_make (fn:A) : Stream A :=
-  let fn1 := g fn in 
+  let fn1 := g fn in
   Cons fn1 (imemo_make fn1).
 
 Definition imemo_list := let f0 := f 0 in
@@ -68,7 +68,7 @@ Qed.
 
 End MemoFunction.
 
-(** For a dependent function, the previous solution is 
+(** For a dependent function, the previous solution is
     reused thanks to a temporarly hiding of the dependency
     in a "container" [memo_val]. *)
 
@@ -88,7 +88,7 @@ Fixpoint is_eq (n m : nat) {struct n}: {n = m} + {True} :=
   | S n1, S m1 =>
      match is_eq n1 m1 with
      | left H => left True (f_equal S H)
-     | right _ => right (S n1 = S m1) I 
+     | right _ => right (S n1 = S m1) I
      end
   end.
 
@@ -134,7 +134,7 @@ Variable g: forall n, A n -> A (S n).
 
 Hypothesis Hg_correct: forall n, f (S n) = g n (f n).
 
-Let mg v :=  match v with 
+Let mg v :=  match v with
              memo_mval n1 v1 => memo_mval (S n1) (g n1 v1) end.
 
 Definition dimemo_list := imemo_list _ mf mg.
@@ -166,13 +166,13 @@ End DependentMemoFunction.
 Require Import ZArith.
 Open Scope Z_scope.
 
-Fixpoint tfact (n: nat) := 
-  match n with 
-   | O => 1 
-   | S n1 => Z_of_nat n * tfact n1 
+Fixpoint tfact (n: nat) :=
+  match n with
+   | O => 1
+   | S n1 => Z_of_nat n * tfact n1
   end.
 
-Definition lfact_list := 
+Definition lfact_list :=
   dimemo_list _ tfact (fun n z => (Z_of_nat (S  n) * z)).
 
 Definition lfact n := dmemo_get _ tfact n lfact_list.
@@ -183,18 +183,18 @@ intros n; unfold lfact, lfact_list.
 rewrite dimemo_get_correct; auto.
 Qed.
 
-Fixpoint nop p := 
+Fixpoint nop p :=
   match p with
-   | xH => 0 
-   | xI p1 => nop p1 
-   | xO p1 => nop p1 
+   | xH => 0
+   | xI p1 => nop p1
+   | xO p1 => nop p1
   end.
 
-Fixpoint test z := 
+Fixpoint test z :=
   match z with
-   | Z0 => 0 
-   | Zpos p1 => nop p1 
-   | Zneg p1 => nop p1 
+   | Z0 => 0
+   | Zpos p1 => nop p1
+   | Zneg p1 => nop p1
   end.
 
 Time Eval vm_compute in test (lfact 2000).
@@ -202,4 +202,4 @@ Time Eval vm_compute in test (lfact 2000).
 Time Eval vm_compute in test (lfact 1500).
 Time Eval vm_compute in (lfact 1500).
 *)
- 
+
diff --git a/theories/Lists/Streams.v b/theories/Lists/Streams.v
index 472265f3e3..ace157749f 100644
--- a/theories/Lists/Streams.v
+++ b/theories/Lists/Streams.v
@@ -41,7 +41,7 @@ Definition Str_nth (n:nat) (s:Stream) : A := hd (Str_nth_tl n s).
 Lemma unfold_Stream :
  forall x:Stream, x = match x with
                       | Cons a s => Cons a s
-                      end. 
+                      end.
 Proof.
   intro x.
   case x.
@@ -223,7 +223,7 @@ Variable f: A -> B -> C.
 CoFixpoint zipWith (a:Stream A) (b:Stream B) : Stream C :=
 Cons (f (hd a) (hd b)) (zipWith (tl a) (tl b)).
 
-Lemma Str_nth_tl_zipWith : forall n (a:Stream A) (b:Stream B), 
+Lemma Str_nth_tl_zipWith : forall n (a:Stream A) (b:Stream B),
  Str_nth_tl n (zipWith a b)= zipWith (Str_nth_tl n a) (Str_nth_tl n b).
 Proof.
 induction n.
diff --git a/theories/Lists/TheoryList.v b/theories/Lists/TheoryList.v
index 226d071499..5185f2c539 100644
--- a/theories/Lists/TheoryList.v
+++ b/theories/Lists/TheoryList.v
@@ -349,7 +349,7 @@ destruct (TS_dec a) as [[c H1]| ].
 left; exists c.
 exists a; auto.
 auto.
-(* 
+(*
 Realizer try_find.
 *)
 Qed.
@@ -359,7 +359,7 @@ End Find_sec.
 Section Assoc_sec.
 
 Variable B : Type.
-Fixpoint assoc (a:A) (l:list (A * B)) {struct l} : 
+Fixpoint assoc (a:A) (l:list (A * B)) {struct l} :
  Exc B :=
   match l with
   | nil => error