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

37 files changed, 105 insertions, 105 deletions

diff --git a/test-suite/bugs/closed/shouldsucceed/1100.v b/test-suite/bugs/closed/shouldsucceed/1100.v
index 6d619c748..32c78b4b9 100644
--- a/test-suite/bugs/closed/shouldsucceed/1100.v
+++ b/test-suite/bugs/closed/shouldsucceed/1100.v
@@ -6,7 +6,7 @@ Parameter PQ : forall n, P n <-> Q n.
 
 Lemma PQ2 : forall n, P n -> Q n.
   intros.
-  rewrite PQ in H. 
+  rewrite PQ in H.
   trivial.
 Qed.
 
diff --git a/test-suite/bugs/closed/shouldsucceed/1322.v b/test-suite/bugs/closed/shouldsucceed/1322.v
index 7e21aa7ce..1ec7d452a 100644
--- a/test-suite/bugs/closed/shouldsucceed/1322.v
+++ b/test-suite/bugs/closed/shouldsucceed/1322.v
@@ -7,7 +7,7 @@ Variable I_eq :I -> I -> Prop.
 Variable I_eq_equiv : Setoid_Theory I I_eq.
 
 (* Add Relation I I_eq
-  reflexivity proved by I_eq_equiv.(Seq_refl I I_eq) 
+  reflexivity proved by I_eq_equiv.(Seq_refl I I_eq)
   symmetry proved by I_eq_equiv.(Seq_sym I I_eq)
   transitivity proved by I_eq_equiv.(Seq_trans I I_eq)
 as I_eq_relation. *)
diff --git a/test-suite/bugs/closed/shouldsucceed/1411.v b/test-suite/bugs/closed/shouldsucceed/1411.v
index e330d46fd..a1a7b288a 100644
--- a/test-suite/bugs/closed/shouldsucceed/1411.v
+++ b/test-suite/bugs/closed/shouldsucceed/1411.v
@@ -23,7 +23,7 @@ Program Fixpoint fetch t p (x:Exact t p) {struct t} :=
    match t, p with
    | No p' , nil      => p'
    | No p' , _::_     => unreachable nat _
-   | Br l r, nil      => unreachable nat _ 
+   | Br l r, nil      => unreachable nat _
    | Br l r, true::t  => fetch l t _
    | Br l r, false::t => fetch r t _
    end.
diff --git a/test-suite/bugs/closed/shouldsucceed/1414.v b/test-suite/bugs/closed/shouldsucceed/1414.v
index 06922e50a..495a16bca 100644
--- a/test-suite/bugs/closed/shouldsucceed/1414.v
+++ b/test-suite/bugs/closed/shouldsucceed/1414.v
@@ -7,8 +7,8 @@ Inductive t : Set :=
   | Node : t -> data -> t -> Z -> t.
 
 Parameter avl : t -> Prop.
-Parameter bst : t -> Prop. 
-Parameter In : data -> t -> Prop. 
+Parameter bst : t -> Prop.
+Parameter In : data -> t -> Prop.
 Parameter cardinal : t -> nat.
 Definition card2 (s:t*t) := let (s1,s2) := s in cardinal s1 + cardinal s2.
 
@@ -16,25 +16,25 @@ Parameter split : data -> t -> t*(bool*t).
 Parameter join : t -> data -> t -> t.
 Parameter add : data -> t -> t.
 
-Program Fixpoint union 
+Program Fixpoint union
   (s u:t)
-  (hb1: bst s)(ha1: avl s)(hb2: bst u)(hb2: avl u) 
-  { measure (cardinal s + cardinal u) } : 
-  {s' : t | bst s' /\ avl s' /\ forall x, In x s' <-> In x s \/ In x u} := 
-  match s, u with 
+  (hb1: bst s)(ha1: avl s)(hb2: bst u)(hb2: avl u)
+  { measure (cardinal s + cardinal u) } :
+  {s' : t | bst s' /\ avl s' /\ forall x, In x s' <-> In x s \/ In x u} :=
+  match s, u with
     | Leaf,t2 => t2
     | t1,Leaf => t1
-    | Node l1 v1 r1 h1, Node l2 v2 r2 h2 =>        
+    | Node l1 v1 r1 h1, Node l2 v2 r2 h2 =>
         if (Z_ge_lt_dec h1 h2) then
-          if (Z_eq_dec h2 1) 
+          if (Z_eq_dec h2 1)
           then add v2 s
           else
             let (l2', r2') := split v1 u in
             join (union l1 l2' _ _ _ _) v1 (union r1 (snd r2') _ _ _ _)
         else
-          if (Z_eq_dec h1 1) 
+          if (Z_eq_dec h1 1)
           then add v1 s
           else
             let (l1', r1') := split v2 u in
             join (union l1' l2 _ _ _ _) v2 (union (snd r1') r2 _ _ _ _)
-  end. 
+  end.
diff --git a/test-suite/bugs/closed/shouldsucceed/1425.v b/test-suite/bugs/closed/shouldsucceed/1425.v
index 8e26209a1..6be30174a 100644
--- a/test-suite/bugs/closed/shouldsucceed/1425.v
+++ b/test-suite/bugs/closed/shouldsucceed/1425.v
@@ -1,4 +1,4 @@
-Require Import Setoid. 
+Require Import Setoid.
 
 Parameter recursion : forall A : Set, A -> (nat -> A -> A) -> nat -> A.
 
diff --git a/test-suite/bugs/closed/shouldsucceed/1446.v b/test-suite/bugs/closed/shouldsucceed/1446.v
index d4e7cea81..8cb2d653b 100644
--- a/test-suite/bugs/closed/shouldsucceed/1446.v
+++ b/test-suite/bugs/closed/shouldsucceed/1446.v
@@ -1,8 +1,8 @@
 Lemma not_true_eq_false : forall (b:bool), b <> true -> b = false.
 Proof.
- destruct b;intros;trivial. 
- elim H. 
- exact (refl_equal true). 
+ destruct b;intros;trivial.
+ elim H.
+ exact (refl_equal true).
 Qed.
 
 Section BUG.
@@ -13,7 +13,7 @@ Section BUG.
  Hypothesis H1 : b <> true.
 
  Goal False.
-  rewrite (not_true_eq_false _ H) in * |-. 
+  rewrite (not_true_eq_false _ H) in * |-.
   contradiction.
  Qed.
 
diff --git a/test-suite/bugs/closed/shouldsucceed/1507.v b/test-suite/bugs/closed/shouldsucceed/1507.v
index 32e6489c5..f1872a2bb 100644
--- a/test-suite/bugs/closed/shouldsucceed/1507.v
+++ b/test-suite/bugs/closed/shouldsucceed/1507.v
@@ -8,10 +8,10 @@
                rational intervals.
 *)
 
-Definition associative (A:Type)(op:A->A->A) := 
+Definition associative (A:Type)(op:A->A->A) :=
   forall x y z:A, op (op x y) z = op x (op y z).
 
-Definition commutative (A:Type)(op:A->A->A) := 
+Definition commutative (A:Type)(op:A->A->A) :=
   forall x y:A, op x y = op y x.
 
 Definition trichotomous (A:Type)(R:A->A->Prop) :=
@@ -19,7 +19,7 @@ Definition trichotomous (A:Type)(R:A->A->Prop) :=
 
 Definition relation (A:Type) := A -> A -> Prop.
 Definition reflexive (A:Type)(R:relation A) := forall x:A, R x x.
-Definition transitive (A:Type)(R:relation A) := 
+Definition transitive (A:Type)(R:relation A) :=
   forall x y z:A, R x y -> R y z -> R x z.
 Definition symmetric (A:Type)(R:relation A) := forall x y:A, R x y -> R y x.
 
@@ -52,7 +52,7 @@ Record I (grnd:Set)(le:grnd->grnd->Prop) : Type := Imake {
   Iplus_opp_r    : forall x:Icar, Ic (Iplus x (Iopp x)) (Izero);
   Imult_inv_r    : forall x:Icar, ~(Ic x Izero) -> Ic (Imult x (Iinv x)) Ione;
   (* distributive laws *)
-  Imult_plus_distr_l : forall x x' y y' z z' z'', 
+  Imult_plus_distr_l : forall x x' y y' z z' z'',
     Ic x x' -> Ic y y' -> Ic z z' -> Ic z z'' ->
     Ic (Imult (Iplus x y) z) (Iplus (Imult x' z') (Imult y' z''));
   (* order and lattice structure *)
@@ -70,7 +70,7 @@ Record I (grnd:Set)(le:grnd->grnd->Prop) : Type := Imake {
   Ic_sym    : symmetric _ Ic
 }.
 
-Definition interval_set (X:Set)(le:X->X->Prop) := 
+Definition interval_set (X:Set)(le:X->X->Prop) :=
   (interval X le) -> Prop. (* can be Set as well *)
 Check interval_set.
 Check Ic.
@@ -101,7 +101,7 @@ Record N (grnd:Set)(le:grnd->grnd->Prop)(grndI:I grnd le) : Type := Nmake {
   Nplus_opp_r    : forall x:Ncar, Nc (Nplus x (Nopp x)) (Nzero);
   Nmult_inv_r    : forall x:Ncar, ~(Nc x Nzero) -> Nc (Nmult x (Ninv x)) None;
   (* distributive laws *)
-  Nmult_plus_distr_l : forall x x' y y' z z' z'', 
+  Nmult_plus_distr_l : forall x x' y y' z z' z'',
     Nc x x' -> Nc y y' -> Nc z z' -> Nc z z'' ->
     Nc (Nmult (Nplus x y) z) (Nplus (Nmult x' z') (Nmult y' z''));
   (* order and lattice structure *)
diff --git a/test-suite/bugs/closed/shouldsucceed/1568.v b/test-suite/bugs/closed/shouldsucceed/1568.v
index 9f10f7490..3609e9c83 100644
--- a/test-suite/bugs/closed/shouldsucceed/1568.v
+++ b/test-suite/bugs/closed/shouldsucceed/1568.v
@@ -3,7 +3,7 @@ CoInductive A: Set :=
 with B: Set :=
   mk_B: A -> B.
 
-CoFixpoint a:A := mk_A b 
+CoFixpoint a:A := mk_A b
 with b:B := mk_B a.
 
 Goal b = match a with mk_A a1 => a1 end.
diff --git a/test-suite/bugs/closed/shouldsucceed/1576.v b/test-suite/bugs/closed/shouldsucceed/1576.v
index c9ebbd142..3621f7a1f 100644
--- a/test-suite/bugs/closed/shouldsucceed/1576.v
+++ b/test-suite/bugs/closed/shouldsucceed/1576.v
@@ -13,8 +13,8 @@ End TC.
 Module Type TD.
 
 Declare Module B: TB .
-Declare Module C: TC 
-    with Module B := B  . 
+Declare Module C: TC
+    with Module B := B  .
 End TD.
 
 Module Type TE.
@@ -25,7 +25,7 @@ Module Type TF.
 Declare Module E:  TE.
 End TF.
 
-Module G (D: TD). 
+Module G (D: TD).
 Module B' := D.C.B.
 End G.
 
diff --git a/test-suite/bugs/closed/shouldsucceed/1582.v b/test-suite/bugs/closed/shouldsucceed/1582.v
index 47953a66f..be5d3dd21 100644
--- a/test-suite/bugs/closed/shouldsucceed/1582.v
+++ b/test-suite/bugs/closed/shouldsucceed/1582.v
@@ -1,12 +1,12 @@
 Require Import Peano_dec.
 
-Definition fact_F : 
+Definition fact_F :
   forall (n:nat),
   (forall m, m<n -> nat) ->
   nat.
-refine 
+refine
   (fun n fact_rec =>
-     if eq_nat_dec n 0 then 
+     if eq_nat_dec n 0 then
         1
      else
         let fn := fact_rec (n-1) _ in
diff --git a/test-suite/bugs/closed/shouldsucceed/1618.v b/test-suite/bugs/closed/shouldsucceed/1618.v
index a90290bfb..a9b067ceb 100644
--- a/test-suite/bugs/closed/shouldsucceed/1618.v
+++ b/test-suite/bugs/closed/shouldsucceed/1618.v
@@ -6,7 +6,7 @@ Definition A_size (a: A) : nat :=
     | A1 n => 0
   end.
 
-Require Import Recdef. 
+Require Import Recdef.
 
 Function n3 (P: A -> Prop) (f: forall n, P (A1 n)) (a: A) {struct a} : P a :=
   match a  return (P a) with
diff --git a/test-suite/bugs/closed/shouldsucceed/1634.v b/test-suite/bugs/closed/shouldsucceed/1634.v
index e0c540f36..0150c2503 100644
--- a/test-suite/bugs/closed/shouldsucceed/1634.v
+++ b/test-suite/bugs/closed/shouldsucceed/1634.v
@@ -18,7 +18,7 @@ Add Parametric Relation a : (S a) Seq
 
 Goal forall (a : A) (x y : S a), Seq x y -> Seq x y.
   intros a x y H.
-  setoid_replace x with y. 
+  setoid_replace x with y.
   reflexivity.
   trivial.
 Qed.
diff --git a/test-suite/bugs/closed/shouldsucceed/1683.v b/test-suite/bugs/closed/shouldsucceed/1683.v
index 1571ee20e..3e99694b3 100644
--- a/test-suite/bugs/closed/shouldsucceed/1683.v
+++ b/test-suite/bugs/closed/shouldsucceed/1683.v
@@ -30,7 +30,7 @@ Add Parametric Relation A : (ms_type A) (ms_eq A)
 Hypothesis foobar : forall n, ms_eq CR (IRasCR (foo IR n)) (foo CRasCRing n).
 
 Goal forall (b:ms_type CR),
- ms_eq CR (IRasCR (foo IR O)) b -> 
+ ms_eq CR (IRasCR (foo IR O)) b ->
  ms_eq CR (IRasCR (foo IR O)) b.
 intros b H.
 rewrite foobar.
diff --git a/test-suite/bugs/closed/shouldsucceed/1738.v b/test-suite/bugs/closed/shouldsucceed/1738.v
index 0deed3663..c2926a2b2 100644
--- a/test-suite/bugs/closed/shouldsucceed/1738.v
+++ b/test-suite/bugs/closed/shouldsucceed/1738.v
@@ -5,10 +5,10 @@ Module SomeSetoids (Import M:FSetInterface.S).
 Lemma Equal_refl : forall s, s[=]s.
 Proof. red; split; auto. Qed.
 
-Add Relation t Equal 
- reflexivity proved by Equal_refl 
+Add Relation t Equal
+ reflexivity proved by Equal_refl
  symmetry proved by eq_sym
- transitivity proved by eq_trans 
+ transitivity proved by eq_trans
  as EqualSetoid.
 
 Add Morphism Empty with signature Equal ==> iff as Empty_m.
diff --git a/test-suite/bugs/closed/shouldsucceed/1740.v b/test-suite/bugs/closed/shouldsucceed/1740.v
index d9ce546a2..ec4a7a6bc 100644
--- a/test-suite/bugs/closed/shouldsucceed/1740.v
+++ b/test-suite/bugs/closed/shouldsucceed/1740.v
@@ -17,7 +17,7 @@ Goal f =
       | n, O => n
       | _, _ => O
     end.
-  unfold f. 
+  unfold f.
   reflexivity.
 Qed.
 
diff --git a/test-suite/bugs/closed/shouldsucceed/1775.v b/test-suite/bugs/closed/shouldsucceed/1775.v
index dab4120b9..932949a37 100644
--- a/test-suite/bugs/closed/shouldsucceed/1775.v
+++ b/test-suite/bugs/closed/shouldsucceed/1775.v
@@ -13,7 +13,7 @@ Goal forall s k k' m,
   (pl k' (nexists (fun w => (nexists (fun b => pl (pair w w)
     (pl (pair s b)
     (nexists (fun w0 => (nexists (fun a => pl (pair b w0)
-      (nexists (fun w1 => (nexists (fun c => pl 
+      (nexists (fun w1 => (nexists (fun c => pl
         (pair a w1) (pl (pair a c) k))))))))))))))) m.
 intros.
 eapply plImp; [ | eauto | intros ].
diff --git a/test-suite/bugs/closed/shouldsucceed/1776.v b/test-suite/bugs/closed/shouldsucceed/1776.v
index abf854553..58491f9de 100644
--- a/test-suite/bugs/closed/shouldsucceed/1776.v
+++ b/test-suite/bugs/closed/shouldsucceed/1776.v
@@ -10,7 +10,7 @@ Definition nexists (P:nat -> nat -> Prop) : nat -> Prop :=
 
 Goal forall a A m,
   True ->
-  (pl A (nexists (fun x => (nexists 
+  (pl A (nexists (fun x => (nexists
     (fun y => pl (pair a (S x)) (pair a (S y))))))) m.
 Proof.
   intros.
diff --git a/test-suite/bugs/closed/shouldsucceed/1784.v b/test-suite/bugs/closed/shouldsucceed/1784.v
index 5855b1683..8c2e50e07 100644
--- a/test-suite/bugs/closed/shouldsucceed/1784.v
+++ b/test-suite/bugs/closed/shouldsucceed/1784.v
@@ -56,16 +56,16 @@ Require Import Program.
 
 Program Fixpoint lt_dec (x y:sv) { struct x } : {slt x y}+{~slt x y} :=
   match x with
-    | I x => 
+    | I x =>
       match y with
         | I y => if (Z_eq_dec x y) then in_left else in_right
         | S ys => in_right
       end
-    | S xs => 
+    | S xs =>
       match y with
         | I y => in_right
         | S ys =>
-          let fix list_in (xs ys:list sv) {struct xs} : 
+          let fix list_in (xs ys:list sv) {struct xs} :
             {slist_in xs ys} + {~slist_in xs ys} :=
             match xs with
               | nil => in_left
@@ -76,8 +76,8 @@ Program Fixpoint lt_dec (x y:sv) { struct x } : {slt x y}+{~slt x y} :=
                     | y::ys => if lt_dec x y then in_left else if elem_in
                       ys then in_left else in_right
                   end
-                in 
-                if elem_in ys then 
+                in
+                if elem_in ys then
                   if list_in xs ys then in_left else in_right
                 else in_right
             end
@@ -90,7 +90,7 @@ Next Obligation. intro H; inversion H. Defined.
 Next Obligation. intro H; inversion H. Defined.
 Next Obligation. intro H; inversion H; subst. Defined.
 Next Obligation.
-  intro H1; contradict H. inversion H1; subst. assumption. 
+  intro H1; contradict H. inversion H1; subst. assumption.
   contradict H0; assumption. Defined.
 Next Obligation.
   intro H1; contradict H0. inversion H1; subst. assumption. Defined.
diff --git a/test-suite/bugs/closed/shouldsucceed/1791.v b/test-suite/bugs/closed/shouldsucceed/1791.v
index 694f056e8..be0e8ae8b 100644
--- a/test-suite/bugs/closed/shouldsucceed/1791.v
+++ b/test-suite/bugs/closed/shouldsucceed/1791.v
@@ -9,7 +9,7 @@ Definition k1 := k0 -> k0.
 (** iterating X n times *)
 Fixpoint Pow (X:k1)(k:nat){struct k}:k1:=
   match k with 0 => fun X => X
-             |  S k' => fun A => X (Pow X k' A)   
+             |  S k' => fun A => X (Pow X k' A)
   end.
 
 Parameter Bush: k1.
diff --git a/test-suite/bugs/closed/shouldsucceed/1844.v b/test-suite/bugs/closed/shouldsucceed/1844.v
index 545f26154..5627612f6 100644
--- a/test-suite/bugs/closed/shouldsucceed/1844.v
+++ b/test-suite/bugs/closed/shouldsucceed/1844.v
@@ -188,7 +188,7 @@ with exec_finish: function -> outcome -> store -> value -> store -> Prop :=
 
 with exec_function: function -> store -> value -> store -> Prop :=
  | exec_function_intro: forall f st out st1 v st',
-     exec f.(fn_body) st out st1 -> 
+     exec f.(fn_body) st out st1 ->
      exec_finish f out st1 v st' ->
      exec_function f st v st'.
 
diff --git a/test-suite/bugs/closed/shouldsucceed/1901.v b/test-suite/bugs/closed/shouldsucceed/1901.v
index 598db3660..7d86adbfb 100644
--- a/test-suite/bugs/closed/shouldsucceed/1901.v
+++ b/test-suite/bugs/closed/shouldsucceed/1901.v
@@ -2,9 +2,9 @@ Require Import Relations.
 
 Record Poset{A:Type}(Le : relation A) : Type :=
   Build_Poset
-  { 
-    Le_refl : forall x : A, Le x x; 
-    Le_trans : forall x y z : A, Le x y -> Le y z -> Le x z; 
+  {
+    Le_refl : forall x : A, Le x x;
+    Le_trans : forall x y z : A, Le x y -> Le y z -> Le x z;
     Le_antisym : forall x y : A, Le x y -> Le y x -> x = y }.
 
 Definition nat_Poset : Poset Peano.le.
diff --git a/test-suite/bugs/closed/shouldsucceed/1905.v b/test-suite/bugs/closed/shouldsucceed/1905.v
index fb2725c97..8c81d7510 100644
--- a/test-suite/bugs/closed/shouldsucceed/1905.v
+++ b/test-suite/bugs/closed/shouldsucceed/1905.v
@@ -5,7 +5,7 @@ Axiom t : Set.
 Axiom In : nat -> t -> Prop.
 Axiom InE : forall (x : nat) (s:t), impl (In x s) True.
 
-Goal forall a s, 
+Goal forall a s,
  In a s -> False.
 Proof.
  intros a s Ia.
diff --git a/test-suite/bugs/closed/shouldsucceed/1918.v b/test-suite/bugs/closed/shouldsucceed/1918.v
index 9d4a3e047..474ec935b 100644
--- a/test-suite/bugs/closed/shouldsucceed/1918.v
+++ b/test-suite/bugs/closed/shouldsucceed/1918.v
@@ -35,7 +35,7 @@ Definition mon (X:k1) : Type := forall (A B:Set), (A -> B) -> X A -> X B.
 
 (** extensionality *)
 Definition ext (X:k1)(h: mon X): Prop :=
-  forall (A B:Set)(f g:A -> B), 
+  forall (A B:Set)(f g:A -> B),
         (forall a, f a = g a) -> forall r, h _ _ f r = h _ _ g r.
 
 (** first functor law *)
@@ -44,7 +44,7 @@ Definition fct1 (X:k1)(m: mon X) : Prop :=
 
 (** second functor law *)
 Definition fct2 (X:k1)(m: mon X) : Prop :=
- forall (A B C:Set)(f:A -> B)(g:B -> C)(x:X A), 
+ forall (A B C:Set)(f:A -> B)(g:B -> C)(x:X A),
        m _ _ (g o f) x = m _ _ g (m _ _ f x).
 
 (** pack up the good properties of the approximation into
@@ -60,7 +60,7 @@ Definition pEFct (F:k2) : Type :=
   forall (X:k1), EFct X -> EFct (F X).
 
 
-(** we show some closure properties of pEFct, depending on such properties 
+(** we show some closure properties of pEFct, depending on such properties
       for EFct *)
 
 Definition moncomp (X Y:k1)(mX:mon X)(mY:mon Y): mon (fun A => X(Y A)).
@@ -92,7 +92,7 @@ Proof.
   apply (f2 ef2).
 Defined.
 
-Corollary comppEFct (F G:k2): pEFct F -> pEFct G -> 
+Corollary comppEFct (F G:k2): pEFct F -> pEFct G ->
       pEFct (fun X A => F X (G X A)).
 Proof.
   red.
@@ -104,7 +104,7 @@ Defined.
 Lemma sumEFct (X Y:k1): EFct X -> EFct Y -> EFct (fun A => X A + Y A)%type.
 Proof.
   intros X Y ef1 ef2.
-  set (m12:=fun (A B:Set)(f:A->B) x => match x with 
+  set (m12:=fun (A B:Set)(f:A->B) x => match x with
     | inl y => inl _ (m ef1 f y)
     | inr y => inr _ (m ef2 f y)
   end).
@@ -133,7 +133,7 @@ Proof.
   rewrite (f2 ef2); reflexivity.
 Defined.
 
-Corollary sumpEFct (F G:k2): pEFct F -> pEFct G -> 
+Corollary sumpEFct (F G:k2): pEFct F -> pEFct G ->
       pEFct (fun X A => F X A + G X A)%type.
 Proof.
   red.
@@ -145,7 +145,7 @@ Defined.
 Lemma prodEFct (X Y:k1): EFct X -> EFct Y -> EFct (fun A => X A * Y A)%type.
 Proof.
   intros X Y ef1 ef2.
-  set (m12:=fun (A B:Set)(f:A->B) x => match x with 
+  set (m12:=fun (A B:Set)(f:A->B) x => match x with
     (x1,x2) => (m ef1 f x1, m ef2 f x2) end).
   apply (mkEFct(m:=m12)); red; intros.
 (* prove ext *)
@@ -168,7 +168,7 @@ Proof.
   apply (f2 ef2).
 Defined.
 
-Corollary prodpEFct (F G:k2): pEFct F -> pEFct G -> 
+Corollary prodpEFct (F G:k2): pEFct F -> pEFct G ->
       pEFct (fun X A => F X A * G X A)%type.
 Proof.
   red.
@@ -248,19 +248,19 @@ Module Type LNMIt_Type.
 
 Parameter F:k2.
 Parameter FpEFct: pEFct F.
-Parameter mu20: k1. 
+Parameter mu20: k1.
 Definition  mu2: k1:= fun A => mu20 A.
 Parameter mapmu2: mon mu2.
 Definition MItType: Type :=
   forall G : k1, (forall X : k1, X c_k1 G -> F X c_k1 G) -> mu2 c_k1 G.
 Parameter MIt0 : MItType.
-Definition MIt : MItType:= fun G s A t => MIt0 s t. 
-Definition InType : Type := 
-    forall (X:k1)(ef:EFct X)(j: X c_k1 mu2), 
+Definition MIt : MItType:= fun G s A t => MIt0 s t.
+Definition InType : Type :=
+    forall (X:k1)(ef:EFct X)(j: X c_k1 mu2),
         NAT j (m ef) mapmu2 -> F X c_k1 mu2.
 Parameter In : InType.
 Axiom mapmu2Red : forall (A:Set)(X:k1)(ef:EFct X)(j: X c_k1 mu2)
-    (n: NAT j (m ef) mapmu2)(t: F X A)(B:Set)(f:A->B), 
+    (n: NAT j (m ef) mapmu2)(t: F X A)(B:Set)(f:A->B),
             mapmu2 f (In ef n t) = In ef n (m (FpEFct ef) f t).
 Axiom MItRed : forall (G : k1)
   (s : forall X : k1, X c_k1 G -> F X c_k1 G)(X : k1)(ef:EFct X)(j: X c_k1 mu2)
@@ -327,8 +327,8 @@ Fixpoint Pow (X:k1)(k:nat){struct k}:k1:=
 
 Fixpoint POW  (k:nat)(X:k1)(m:mon X){struct k} : mon (Pow X k) :=
   match k return mon (Pow X k)
-      with 0 => fun _ _ f  => f 
-     |  S k' => fun _ _ f  => m _ _ (POW k' m f) 
+      with 0 => fun _ _ f  => f
+     |  S k' => fun _ _ f  => m _ _ (POW k' m f)
    end.
 
 Module Type BushkToList_Type.
diff --git a/test-suite/bugs/closed/shouldsucceed/1925.v b/test-suite/bugs/closed/shouldsucceed/1925.v
index 17eb721ad..4caee1c36 100644
--- a/test-suite/bugs/closed/shouldsucceed/1925.v
+++ b/test-suite/bugs/closed/shouldsucceed/1925.v
@@ -3,14 +3,14 @@
 
 Require Import List.
 
-Definition compose (A B C : Type) (g : B -> C) (f : A -> B) : A -> C := 
+Definition compose (A B C : Type) (g : B -> C) (f : A -> B) : A -> C :=
   fun x : A => g(f x).
 
-Definition map_fuse' : 
-  forall (A B C : Type) (g : B -> C) (f : A -> B) (xs : list A), 
-    (map g (map f xs)) = map (compose _ _ _ g f) xs 
+Definition map_fuse' :
+  forall (A B C : Type) (g : B -> C) (f : A -> B) (xs : list A),
+    (map g (map f xs)) = map (compose _ _ _ g f) xs
     :=
-    fun A B C g f => 
+    fun A B C g f =>
       (fix loop (ys : list A) {struct ys} :=
         match ys as ys return (map g (map f ys)) = map (compose _ _ _ g f) ys
         with
diff --git a/test-suite/bugs/closed/shouldsucceed/1931.v b/test-suite/bugs/closed/shouldsucceed/1931.v
index bc8be78fe..930ace1d5 100644
--- a/test-suite/bugs/closed/shouldsucceed/1931.v
+++ b/test-suite/bugs/closed/shouldsucceed/1931.v
@@ -8,7 +8,7 @@ Inductive T (A:Set) : Set :=
 Fixpoint map (A B:Set)(f:A->B)(t:T A) : T B :=
  match t with
    app t1 t2 => app (map f t1)(map f t2)
- end. 
+ end.
 
 Fixpoint subst (A B:Set)(f:A -> T B)(t:T A) :T B :=
  match t with
@@ -19,7 +19,7 @@ Fixpoint subst (A B:Set)(f:A -> T B)(t:T A) :T B :=
 Definition k0:=Set.
 
 (** interaction of subst with map *)
-Lemma substLaw1 (A:k0)(B C:Set)(f: A -> B)(g:B -> T C)(t: T A): 
+Lemma substLaw1 (A:k0)(B C:Set)(f: A -> B)(g:B -> T C)(t: T A):
  subst g (map f t) = subst (fun x => g (f x)) t.
 Proof.
  intros.
diff --git a/test-suite/bugs/closed/shouldsucceed/1935.v b/test-suite/bugs/closed/shouldsucceed/1935.v
index 641dcb7af..72396d490 100644
--- a/test-suite/bugs/closed/shouldsucceed/1935.v
+++ b/test-suite/bugs/closed/shouldsucceed/1935.v
@@ -1,14 +1,14 @@
 Definition f  (n:nat) := n = n.
 
 Lemma f_refl : forall n , f n.
-intros. reflexivity. 
+intros. reflexivity.
 Qed.
 
 Definition f'  (x:nat) (n:nat) := n = n.
 
 Lemma f_refl' : forall n , f' n n.
 Proof.
- intros. reflexivity. 
+ intros. reflexivity.
 Qed.
 
 Require Import ZArith.
diff --git a/test-suite/bugs/closed/shouldsucceed/1939.v b/test-suite/bugs/closed/shouldsucceed/1939.v
index 3aa55e834..5e61529b4 100644
--- a/test-suite/bugs/closed/shouldsucceed/1939.v
+++ b/test-suite/bugs/closed/shouldsucceed/1939.v
@@ -14,6 +14,6 @@ Require Import Setoid Program.Basics.
  Goal forall x y, R x y -> P y -> P x.
  Proof.
    intros x y H1 H2.
-   rewrite H1. 
+   rewrite H1.
    auto.
  Qed.
\ No newline at end of file
diff --git a/test-suite/bugs/closed/shouldsucceed/1944.v b/test-suite/bugs/closed/shouldsucceed/1944.v
index 7d9f9eb26..ee2918c6e 100644
--- a/test-suite/bugs/closed/shouldsucceed/1944.v
+++ b/test-suite/bugs/closed/shouldsucceed/1944.v
@@ -1,6 +1,6 @@
 (* Test some uses of ? in introduction patterns *)
 
-Inductive J : nat -> Prop := 
+Inductive J : nat -> Prop :=
   | K : forall p, J p -> (True /\ True)  -> J (S p).
 
 Lemma bug : forall n, J n -> J (S n).
diff --git a/test-suite/bugs/closed/shouldsucceed/1951.v b/test-suite/bugs/closed/shouldsucceed/1951.v
index 4fbd6b22d..12c0ef9bf 100644
--- a/test-suite/bugs/closed/shouldsucceed/1951.v
+++ b/test-suite/bugs/closed/shouldsucceed/1951.v
@@ -28,7 +28,7 @@ Inductive sg : Type := Sg. (* single *)
 Definition ipl2 (P : a -> Type) :=   (* in Prop, that means P is true forall *)
 fold_right (fun x => prod (P x)) sg. (* the elements of a given list         *)
 
-Definition ind 
+Definition ind
      : forall S : a -> Type,
        (forall ls : list a, ipl2 S ls -> S (b ls)) -> forall s : a, S s :=
 fun (S : a -> Type)
diff --git a/test-suite/bugs/closed/shouldsucceed/1981.v b/test-suite/bugs/closed/shouldsucceed/1981.v
index 0c3b96dad..99952682d 100644
--- a/test-suite/bugs/closed/shouldsucceed/1981.v
+++ b/test-suite/bugs/closed/shouldsucceed/1981.v
@@ -1,5 +1,5 @@
 Implicit Arguments ex_intro [A].
 
 Goal exists n : nat, True.
-  eapply ex_intro. exact 0. exact I. 
+  eapply ex_intro. exact 0. exact I.
 Qed.
diff --git a/test-suite/bugs/closed/shouldsucceed/2001.v b/test-suite/bugs/closed/shouldsucceed/2001.v
index 323021dea..c50ad036d 100644
--- a/test-suite/bugs/closed/shouldsucceed/2001.v
+++ b/test-suite/bugs/closed/shouldsucceed/2001.v
@@ -2,7 +2,7 @@
    computed when the user explicitly indicated it *)
 
 Inductive T : Set :=
-| v : T. 
+| v : T.
 
 Definition f (s:nat) (t:T) : nat.
 fix 2.
@@ -12,9 +12,9 @@ refine
   | v => s
   end.
 Defined.
-           
+
 Lemma test :
   forall s, f s v = s.
-Proof.    
+Proof.
 reflexivity.
-Qed.        
+Qed.
diff --git a/test-suite/bugs/closed/shouldsucceed/2017.v b/test-suite/bugs/closed/shouldsucceed/2017.v
index 948cea3ee..df6661483 100644
--- a/test-suite/bugs/closed/shouldsucceed/2017.v
+++ b/test-suite/bugs/closed/shouldsucceed/2017.v
@@ -8,8 +8,8 @@ Set Implicit Arguments.
 Variable choose : forall(P : bool -> Prop)(H : exists x, P x), bool.
 
 Variable H : exists x : bool, True.
- 
+
 Definition coef :=
 match Some true	with
-  Some _ => @choose _ H |_ => true 
-end .      
+  Some _ => @choose _ H |_ => true
+end .
diff --git a/test-suite/bugs/closed/shouldsucceed/2083.v b/test-suite/bugs/closed/shouldsucceed/2083.v
index 63f91e565..6fc046495 100644
--- a/test-suite/bugs/closed/shouldsucceed/2083.v
+++ b/test-suite/bugs/closed/shouldsucceed/2083.v
@@ -2,11 +2,11 @@ Require Import Program Arith.
 
 Program Fixpoint check_n  (n : nat) (P : { i | i < n } -> bool) (p : nat)
   (H : forall (i : { i | i < n }), i < p -> P i = true)
-  {measure (n - p)} : 
+  {measure (n - p)} :
   Exc (forall (p : { i | i < n}), P p = true) :=
   match le_lt_dec n p with
   | left _ => value _
-  | right cmp => 
+  | right cmp =>
       if dec (P p) then
         check_n n P (S p) _
       else
diff --git a/test-suite/bugs/closed/shouldsucceed/2117.v b/test-suite/bugs/closed/shouldsucceed/2117.v
index 763d85e2c..6377a8b74 100644
--- a/test-suite/bugs/closed/shouldsucceed/2117.v
+++ b/test-suite/bugs/closed/shouldsucceed/2117.v
@@ -44,7 +44,7 @@ Ltac Subst := apply substcopy;intros;EtaLong.
 Ltac Rigid_aux := fun A => apply A|| Rigid_aux (copyr_fun _ _ _ _ A).
 Ltac Rigid := fun A => apply copyr_atom; Rigid_aux A.
 
-Theorem church0: forall i:Type, exists X:(i->i)->i->i, 
+Theorem church0: forall i:Type, exists X:(i->i)->i->i,
 copy ((i->i)->i->i) (fun f:i->i => fun x:i=>f (X f x)) (fun f:i->i=>fun x:i=>app i i (X f) (f x)).
 intros.
 esplit.
diff --git a/test-suite/bugs/closed/shouldsucceed/2139.v b/test-suite/bugs/closed/shouldsucceed/2139.v
index 4f71d097f..415a1b27d 100644
--- a/test-suite/bugs/closed/shouldsucceed/2139.v
+++ b/test-suite/bugs/closed/shouldsucceed/2139.v
@@ -2,19 +2,19 @@
 
 Class Patch (patch : Type) := {
     commute : patch -> patch -> Prop
-}.  
-    
+}.
+
 Parameter flip : forall	`{patchInstance	: Patch	patch}
-                       	 {a b : patch},	
+                       	 {a b : patch},
                  commute a b <-> commute b a.
-                 
+
 Lemma Foo : forall `{patchInstance : Patch patch}
-                    {a b : patch}, 
+                    {a b : patch},
             (commute a b)
          -> True.
-Proof.   
-intros.  
-apply flip in H. 
+Proof.
+intros.
+apply flip in H.
 
 (* failed in well-formed arity check because elimination predicate of
    iff in (@flip _ _ _ _) had normalized evars while the ones in the
diff --git a/test-suite/bugs/closed/shouldsucceed/38.v b/test-suite/bugs/closed/shouldsucceed/38.v
index 7bc04b1fe..4fc8d7c97 100644
--- a/test-suite/bugs/closed/shouldsucceed/38.v
+++ b/test-suite/bugs/closed/shouldsucceed/38.v
@@ -6,7 +6,7 @@ Inductive liste : Set :=
 | vide : liste
 | c : A -> liste -> liste.
 
-Inductive e : A -> liste -> Prop := 
+Inductive e : A -> liste -> Prop :=
 | ec : forall (x : A) (l : liste), e x (c x l)
 | ee : forall (x y : A) (l : liste), e x l -> e x (c y l).
 
diff --git a/test-suite/bugs/closed/shouldsucceed/846.v b/test-suite/bugs/closed/shouldsucceed/846.v
index a963b225f..ee5ec1fa6 100644
--- a/test-suite/bugs/closed/shouldsucceed/846.v
+++ b/test-suite/bugs/closed/shouldsucceed/846.v
@@ -27,7 +27,7 @@ Definition index := list bool.
 
 Inductive L (A:Set) : index -> Set :=
   initL: A -> L A nil
-  | pluslL: forall l:index, One -> L A (false::l) 
+  | pluslL: forall l:index, One -> L A (false::l)
   | plusrL: forall l:index, L A l -> L A (false::l)
   | varL: forall l:index, L A l -> L A (true::l)
   | appL: forall l:index, L A (true::l) -> L A (true::l) -> L A (true::l)
@@ -109,7 +109,7 @@ Proof.
   exact (monL (fun x:One + A =>
     (match (maybe (fun a:A => initL a) x) with
        | inl u => pluslL _ _ u
-       | inr t' => plusrL t' end)) r). 
+       | inr t' => plusrL t' end)) r).
 Defined.
 
 Section minimal.
@@ -119,11 +119,11 @@ Hypothesis G: Set -> Set.
 Hypothesis step: sub1 (LamF' G) G.
 
 Fixpoint L'(A:Set)(i:index){struct i} : Set :=
-  match i with 
+  match i with
     nil => A
     | false::l => One + L' A l
     | true::l => G (L' A l)
-  end. 
+  end.
 
 Definition LinL': forall (A:Set)(i:index), L A i -> L' A i.
 Proof.
@@ -177,7 +177,7 @@ Proof.
   assumption.
   induction a.
   simpl L' in t.
-  apply (aczelapp (l1:=true::nil) (l2:=i)). 
+  apply (aczelapp (l1:=true::nil) (l2:=i)).
   exact (lam' IHi t).
   simpl L' in t.
   induction t.