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

12 files changed, 24 insertions, 24 deletions

diff --git a/test-suite/failure/Case5.v b/test-suite/failure/Case5.v
index 29996fd451..494443f1c9 100644
--- a/test-suite/failure/Case5.v
+++ b/test-suite/failure/Case5.v
@@ -1,7 +1,7 @@
 Inductive MS : Set :=
   | X : MS -> MS
   | Y : MS -> MS.
- 
+
 Type (fun p : MS => match p return nat with
                     | X x => 0
                     end).
diff --git a/test-suite/failure/Case9.v b/test-suite/failure/Case9.v
index a3b99f6314..d63c49403b 100644
--- a/test-suite/failure/Case9.v
+++ b/test-suite/failure/Case9.v
@@ -1,7 +1,7 @@
 Parameter compare : forall n m : nat, {n < m} + {n = m} + {n > m}.
 Type
   match compare 0 0 return nat with
-  
+
       (* k<i *) | left _ _ (left _ _ _) => 0
    (* k=i *) | left _ _ _ => 0
    (* k>i *) | right _ _ _ => 0
diff --git a/test-suite/failure/guard.v b/test-suite/failure/guard.v
index 7e07a90585..75e5113860 100644
--- a/test-suite/failure/guard.v
+++ b/test-suite/failure/guard.v
@@ -18,4 +18,4 @@ Definition f :=
   let h := f in (* h = Rel 4 *)
   fix F (n:nat) : nat :=
   h F S n. (* here Rel 4 = g *)
-  
+
diff --git a/test-suite/failure/inductive3.v b/test-suite/failure/inductive3.v
index e5a4e1b66c..cf035edf79 100644
--- a/test-suite/failure/inductive3.v
+++ b/test-suite/failure/inductive3.v
@@ -1,4 +1,4 @@
-(* Check that the nested inductive types positivity check avoids recursively 
+(* Check that the nested inductive types positivity check avoids recursively
    non uniform parameters (at least if these parameters break positivity) *)
 
 Inductive t (A:Type) : Type := c : t (A -> A) -> t A.
diff --git a/test-suite/failure/proofirrelevance.v b/test-suite/failure/proofirrelevance.v
index eedf2612b3..93e159e8bd 100644
--- a/test-suite/failure/proofirrelevance.v
+++ b/test-suite/failure/proofirrelevance.v
@@ -1,5 +1,5 @@
 (* This was working in version 8.1beta (bug in the Sort-polymorphism
-   of inductive types), but this is inconsistent with classical logic 
+   of inductive types), but this is inconsistent with classical logic
    in Prop *)
 
 Inductive bool_in_prop : Type := hide : bool -> bool_in_prop
diff --git a/test-suite/failure/rewrite_in_hyp2.v b/test-suite/failure/rewrite_in_hyp2.v
index a32037a21a..1533966efe 100644
--- a/test-suite/failure/rewrite_in_hyp2.v
+++ b/test-suite/failure/rewrite_in_hyp2.v
@@ -1,4 +1,4 @@
-(* Until revision 10221, rewriting in hypotheses of the form 
+(* Until revision 10221, rewriting in hypotheses of the form
    "(fun x => phi(x)) t" with "t" not rewritable used to behave as a
    beta-normalization tactic instead of raising the expected message
    "nothing to rewrite" *)
diff --git a/test-suite/failure/subtyping.v b/test-suite/failure/subtyping.v
index 35fd20369f..127da85133 100644
--- a/test-suite/failure/subtyping.v
+++ b/test-suite/failure/subtyping.v
@@ -4,17 +4,17 @@ Module Type T.
 
  Parameter A : Type.
 
- Inductive L : Prop := 
+ Inductive L : Prop :=
  | L0
  | L1 :  (A -> Prop) -> L.
 
 End T.
 
-Module TT : T. 
+Module TT : T.
 
  Parameter A : Type.
 
- Inductive L : Type := 
+ Inductive L : Type :=
  | L0
  | L1 :  (A -> Prop) -> L.
 
diff --git a/test-suite/failure/subtyping2.v b/test-suite/failure/subtyping2.v
index 0a75ae4565..addd3b459f 100644
--- a/test-suite/failure/subtyping2.v
+++ b/test-suite/failure/subtyping2.v
@@ -61,7 +61,7 @@ End Inverse_Image.
 
 Section Burali_Forti_Paradox.
 
-  Definition morphism (A : Type) (R : A -> A -> Prop) 
+  Definition morphism (A : Type) (R : A -> A -> Prop)
     (B : Type) (S : B -> B -> Prop) (f : A -> B) :=
     forall x y : A, R x y -> S (f x) (f y).
 
@@ -69,7 +69,7 @@ Section Burali_Forti_Paradox.
      assumes there exists an universal system of notations, i.e:
       - A type A0
       - An injection i0 from relations on any type into A0
-      - The proof that i0 is injective modulo morphism 
+      - The proof that i0 is injective modulo morphism
    *)
   Variable A0 : Type.                     (* Type_i *)
   Variable i0 : forall X : Type, (X -> X -> Prop) -> A0. (* X: Type_j *)
@@ -82,7 +82,7 @@ Section Burali_Forti_Paradox.
   (* Embedding of x in y: x and y are images of 2 well founded relations
      R1 and R2, the ordinal of R2 being strictly greater than that of R1.
    *)
-  Record emb (x y : A0) : Prop := 
+  Record emb (x y : A0) : Prop :=
     {X1 : Type;
      R1 : X1 -> X1 -> Prop;
      eqx : x = i0 X1 R1;
@@ -166,7 +166,7 @@ Defined.
 End Subsets.
 
 
-  Definition fsub (a b : A0) (H : emb a b) (x : sub a) : 
+  Definition fsub (a b : A0) (H : emb a b) (x : sub a) :
     sub b := Build_sub _ (witness _ x) (emb_trans _ _ _ (emb_wit _ x) H).
 
   (* F is a morphism: a < b => F(a) < F(b)
diff --git a/test-suite/failure/univ_include.v b/test-suite/failure/univ_include.v
index 4be70d888c..56f04f9d60 100644
--- a/test-suite/failure/univ_include.v
+++ b/test-suite/failure/univ_include.v
@@ -1,9 +1,9 @@
 Definition T := Type.
 Definition U := Type.
 
-Module Type MT. 
+Module Type MT.
   Parameter t : T.
-End MT. 
+End MT.
 
 Module Type MU.
   Parameter t : U.
diff --git a/test-suite/failure/universes-buraliforti-redef.v b/test-suite/failure/universes-buraliforti-redef.v
index 049f97f221..034b7f0947 100644
--- a/test-suite/failure/universes-buraliforti-redef.v
+++ b/test-suite/failure/universes-buraliforti-redef.v
@@ -64,7 +64,7 @@ End Inverse_Image.
 
 Section Burali_Forti_Paradox.
 
-  Definition morphism (A : Type) (R : A -> A -> Prop) 
+  Definition morphism (A : Type) (R : A -> A -> Prop)
     (B : Type) (S : B -> B -> Prop) (f : A -> B) :=
     forall x y : A, R x y -> S (f x) (f y).
 
@@ -72,7 +72,7 @@ Section Burali_Forti_Paradox.
      assumes there exists an universal system of notations, i.e:
       - A type A0
       - An injection i0 from relations on any type into A0
-      - The proof that i0 is injective modulo morphism 
+      - The proof that i0 is injective modulo morphism
    *)
   Variable A0 : Type.                     (* Type_i *)
   Variable i0 : forall X : Type, (X -> X -> Prop) -> A0. (* X: Type_j *)
@@ -85,7 +85,7 @@ Section Burali_Forti_Paradox.
   (* Embedding of x in y: x and y are images of 2 well founded relations
      R1 and R2, the ordinal of R2 being strictly greater than that of R1.
    *)
-  Record emb (x y : A0) : Prop := 
+  Record emb (x y : A0) : Prop :=
     {X1 : Type;
      R1 : X1 -> X1 -> Prop;
      eqx : x = i0 X1 R1;
@@ -168,7 +168,7 @@ Defined.
 End Subsets.
 
 
-  Definition fsub (a b : A0) (H : emb a b) (x : sub a) : 
+  Definition fsub (a b : A0) (H : emb a b) (x : sub a) :
     sub b := Build_sub _ (witness _ x) (emb_trans _ _ _ (emb_wit _ x) H).
 
   (* F is a morphism: a < b => F(a) < F(b)
diff --git a/test-suite/failure/universes-buraliforti.v b/test-suite/failure/universes-buraliforti.v
index d18d211951..1f96ab34a2 100644
--- a/test-suite/failure/universes-buraliforti.v
+++ b/test-suite/failure/universes-buraliforti.v
@@ -47,7 +47,7 @@ End Inverse_Image.
 
 Section Burali_Forti_Paradox.
 
-  Definition morphism (A : Type) (R : A -> A -> Prop) 
+  Definition morphism (A : Type) (R : A -> A -> Prop)
     (B : Type) (S : B -> B -> Prop) (f : A -> B) :=
     forall x y : A, R x y -> S (f x) (f y).
 
@@ -55,7 +55,7 @@ Section Burali_Forti_Paradox.
      assumes there exists an universal system of notations, i.e:
       - A type A0
       - An injection i0 from relations on any type into A0
-      - The proof that i0 is injective modulo morphism 
+      - The proof that i0 is injective modulo morphism
    *)
   Variable A0 : Type.                     (* Type_i *)
   Variable i0 : forall X : Type, (X -> X -> Prop) -> A0. (* X: Type_j *)
@@ -68,7 +68,7 @@ Section Burali_Forti_Paradox.
   (* Embedding of x in y: x and y are images of 2 well founded relations
      R1 and R2, the ordinal of R2 being strictly greater than that of R1.
    *)
-  Record emb (x y : A0) : Prop := 
+  Record emb (x y : A0) : Prop :=
     {X1 : Type;
      R1 : X1 -> X1 -> Prop;
      eqx : x = i0 X1 R1;
@@ -152,7 +152,7 @@ Defined.
 End Subsets.
 
 
-  Definition fsub (a b : A0) (H : emb a b) (x : sub a) : 
+  Definition fsub (a b : A0) (H : emb a b) (x : sub a) :
     sub b := Build_sub _ (witness _ x) (emb_trans _ _ _ (emb_wit _ x) H).
 
   (* F is a morphism: a < b => F(a) < F(b)
diff --git a/test-suite/failure/universes3.v b/test-suite/failure/universes3.v
index 427cec1907..8fb414d5ae 100644
--- a/test-suite/failure/universes3.v
+++ b/test-suite/failure/universes3.v
@@ -15,7 +15,7 @@ Inductive I (B:Type (*6*)) := C : B -> impl Prop (I B).
        where Type(7) is the auxiliary level used to infer the type of I
 *)
 
-(* We cannot enforce Type1 < Type(6) while we already have 
+(* We cannot enforce Type1 < Type(6) while we already have
    Type(6) <= Type(7) < Type3 < Type1 *)
 Definition J := I Type1.