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

14 files changed, 47 insertions, 47 deletions

diff --git a/test-suite/modules/PO.v b/test-suite/modules/PO.v
index 354c3957f..71d331772 100644
--- a/test-suite/modules/PO.v
+++ b/test-suite/modules/PO.v
@@ -7,11 +7,11 @@ Implicit Arguments snd.
 Module Type PO.
   Parameter T : Set.
   Parameter le : T -> T -> Prop.
-  
+
   Axiom le_refl : forall x : T, le x x.
   Axiom le_trans : forall x y z : T, le x y -> le y z -> le x z.
   Axiom le_antis : forall x y : T, le x y -> le y x -> x = y.
-  
+
   Hint Resolve le_refl le_trans le_antis.
 End PO.
 
@@ -28,10 +28,10 @@ Module Pair (X: PO) (Y: PO) <: PO.
 
   Lemma le_trans : forall p1 p2 p3 : T, le p1 p2 -> le p2 p3 -> le p1 p3.
     unfold le in |- *;  intuition; info  eauto.
-  Qed.    
+  Qed.
 
   Lemma le_antis : forall p1 p2 : T, le p1 p2 -> le p2 p1 -> p1 = p2.
-    destruct p1.  
+    destruct p1.
     destruct p2.
     unfold le in |- *.
      intuition.
diff --git a/test-suite/modules/Przyklad.v b/test-suite/modules/Przyklad.v
index 014f6c604..e3694b818 100644
--- a/test-suite/modules/Przyklad.v
+++ b/test-suite/modules/Przyklad.v
@@ -1,4 +1,4 @@
-Definition ifte (T : Set) (A B : Prop) (s : {A} + {B}) 
+Definition ifte (T : Set) (A B : Prop) (s : {A} + {B})
   (th el : T) := if s then th else el.
 
 Implicit Arguments ifte.
@@ -33,7 +33,7 @@ Module Type ELEM.
   Parameter T : Set.
   Parameter eq_dec : forall a a' : T, {a = a'} + {a <> a'}.
 End ELEM.
-                                        
+
 Module Type SET (Elt: ELEM).
   Parameter T : Set.
   Parameter empty : T.
@@ -104,11 +104,11 @@ Module Nat.
 End Nat.
 
 
-Module SetNat := F Nat. 
+Module SetNat := F Nat.
 
 
-Lemma no_zero_in_empty : SetNat.find 0 SetNat.empty = false. 
-apply SetNat.find_empty_false. 
+Lemma no_zero_in_empty : SetNat.find 0 SetNat.empty = false.
+apply SetNat.find_empty_false.
 Qed.
 
 (***************************************************************************)
@@ -120,8 +120,8 @@ Module Lemmas (G: SET) (E: ELEM).
    forall (S : ESet.T) (a1 a2 : E.T),
    let S1 := ESet.add a1 (ESet.add a2 S) in
    let S2 := ESet.add a2 (ESet.add a1 S) in
-   forall a : E.T, ESet.find a S1 = ESet.find a S2. 
-  
+   forall a : E.T, ESet.find a S1 = ESet.find a S2.
+
     intros.
     unfold S1, S2 in |- *.
     elim (E.eq_dec a a1); elim (E.eq_dec a a2); intros H1 H2;
@@ -137,10 +137,10 @@ Inductive list (A : Set) : Set :=
   | nil : list A
   | cons : A -> list A -> list A.
 
-Module ListDict (E: ELEM). 
+Module ListDict (E: ELEM).
   Definition T := list E.T.
   Definition elt := E.T.
-   
+
   Definition empty := nil elt.
   Definition add (e : elt) (s : T) := cons elt e s.
   Fixpoint find (e : elt) (s : T) {struct s} : bool :=
@@ -160,7 +160,7 @@ Module ListDict (E: ELEM).
     auto.
 
   Qed.
-  
+
 
   Lemma find_add_false :
    forall (s : T) (e e' : E.T), e <> e' -> find e (add e' s) = find e s.
@@ -171,8 +171,8 @@ Module ListDict (E: ELEM).
      rewrite H0.
     simpl in |- *.
     reflexivity.
-  Qed.    
-  
+  Qed.
+
 
 End ListDict.
 
diff --git a/test-suite/modules/Tescik.v b/test-suite/modules/Tescik.v
index 8dadace77..1d1b1e0ab 100644
--- a/test-suite/modules/Tescik.v
+++ b/test-suite/modules/Tescik.v
@@ -7,20 +7,20 @@ End ELEM.
 Module Nat.
     Definition A := nat.
     Definition x := 0.
-End Nat. 
+End Nat.
 
 Module List (X: ELEM).
   Inductive list : Set :=
     | nil : list
     | cons : X.A -> list -> list.
- 
+
   Definition head (l : list) := match l with
                                 | nil => X.x
                                 | cons x _ => x
                                 end.
 
   Definition singl (x : X.A) := cons x nil.
-  
+
   Lemma head_singl : forall x : X.A, head (singl x) = x.
   auto.
   Qed.
diff --git a/test-suite/modules/fun_objects.v b/test-suite/modules/fun_objects.v
index f4dc19b3e..dce2ffd50 100644
--- a/test-suite/modules/fun_objects.v
+++ b/test-suite/modules/fun_objects.v
@@ -4,7 +4,7 @@ Unset Strict Implicit.
 Module Type SIG.
   Parameter id : forall A : Set, A -> A.
 End SIG.
- 
+
 Module M (X: SIG).
   Definition idid := X.id X.id.
   Definition id := idid X.id.
diff --git a/test-suite/modules/injection_discriminate_inversion.v b/test-suite/modules/injection_discriminate_inversion.v
index 88c19cb1a..d4ac7b3a2 100644
--- a/test-suite/modules/injection_discriminate_inversion.v
+++ b/test-suite/modules/injection_discriminate_inversion.v
@@ -7,18 +7,18 @@ Module M1 := M.
 
 Goal forall x, M.C x = M1.C 0 -> x = 0 .
   intros x H.
-  (* 
-     injection sur deux constructeurs egaux mais appeles 
-     par des modules differents 
+  (*
+     injection sur deux constructeurs egaux mais appeles
+     par des modules differents
      *)
-  injection H. 
+  injection H.
   tauto.
 Qed.
 
 Goal  M.C 0 <> M1.C 1.
-  (* 
-     Discriminate sur deux constructeurs egaux mais appeles 
-     par des modules differents 
+  (*
+     Discriminate sur deux constructeurs egaux mais appeles
+     par des modules differents
      *)
   intro H;discriminate H.
 Qed.
@@ -26,9 +26,9 @@ Qed.
 
 Goal forall x,  M.C x = M1.C 0 -> x = 0.
   intros x H.
-  (* 
-     inversion sur deux constructeurs egaux mais appeles 
-     par des modules differents 
+  (*
+     inversion sur deux constructeurs egaux mais appeles
+     par des modules differents
      *)
   inversion H. reflexivity.
 Qed.
\ No newline at end of file
diff --git a/test-suite/modules/mod_decl.v b/test-suite/modules/mod_decl.v
index b886eb59d..8b40213a4 100644
--- a/test-suite/modules/mod_decl.v
+++ b/test-suite/modules/mod_decl.v
@@ -31,17 +31,17 @@ Module Type T.
   Module M0.
     Axiom A : Set.
   End M0.
-  
+
   Declare Module M1: SIG.
-  
+
   Module M2 <: SIG.
     Definition A := nat.
   End M2.
-  
+
   Module M3 := M0.
-  
+
   Module M4 : SIG := M0.
-  
+
   Module M5 <: SIG := M0.
 
   Module M6 := F M0.
diff --git a/test-suite/modules/modeq.v b/test-suite/modules/modeq.v
index 45cf9f124..1238ee9de 100644
--- a/test-suite/modules/modeq.v
+++ b/test-suite/modules/modeq.v
@@ -19,4 +19,4 @@ Module Z.
   Module N := M.
 End Z.
 
-Module A : SIG := Z.  
\ No newline at end of file
+Module A : SIG := Z.
\ No newline at end of file
diff --git a/test-suite/modules/modul.v b/test-suite/modules/modul.v
index 9d24d6ce4..36a542ef0 100644
--- a/test-suite/modules/modul.v
+++ b/test-suite/modules/modul.v
@@ -6,7 +6,7 @@ Module M.
   Hint Resolve w.
 
   (* <Warning> : Grammar is replaced by Notation *)
-  
+
   Print Hint *.
 
   Lemma w1 : rel 0 1.
diff --git a/test-suite/modules/obj.v b/test-suite/modules/obj.v
index 97337a125..fda1a074a 100644
--- a/test-suite/modules/obj.v
+++ b/test-suite/modules/obj.v
@@ -1,7 +1,7 @@
 Set Implicit Arguments.
 Unset Strict Implicit.
 
-Module M. 
+Module M.
   Definition a (s : Set) := s.
   Print a.
 End M.
diff --git a/test-suite/modules/objects.v b/test-suite/modules/objects.v
index 070f859ea..d3a4c0b05 100644
--- a/test-suite/modules/objects.v
+++ b/test-suite/modules/objects.v
@@ -2,7 +2,7 @@ Module Type SET.
   Axiom T : Set.
   Axiom x : T.
 End SET.
- 
+
 Set Implicit Arguments.
 Unset Strict Implicit.
 
diff --git a/test-suite/modules/objects2.v b/test-suite/modules/objects2.v
index e286609e5..220e2b369 100644
--- a/test-suite/modules/objects2.v
+++ b/test-suite/modules/objects2.v
@@ -4,7 +4,7 @@
 
 (* Bug #1118 (simplified version), submitted by Evelyne Contejean
   (used to failed in pre-V8.1 trunk because of a call to lookup_mind
-   for structure objects) 
+   for structure objects)
 *)
 
 Module Type S. Record t : Set := { a : nat; b : nat }. End S.
diff --git a/test-suite/modules/sig.v b/test-suite/modules/sig.v
index 4cb6291df..da5d25fa2 100644
--- a/test-suite/modules/sig.v
+++ b/test-suite/modules/sig.v
@@ -18,8 +18,8 @@ Module Type SPRYT.
   End N.
 End SPRYT.
 
-Module K : SPRYT := N.  
-Module K' : SPRYT := M.  
+Module K : SPRYT := N.
+Module K' : SPRYT := M.
 
 Module Type SIG.
   Definition T : Set := M.N.T.
diff --git a/test-suite/modules/sub_objects.v b/test-suite/modules/sub_objects.v
index 5eec07758..fdfd09f80 100644
--- a/test-suite/modules/sub_objects.v
+++ b/test-suite/modules/sub_objects.v
@@ -12,7 +12,7 @@ Module M.
   Module N.
     Definition idid (A : Set) (x : A) := id x.
     (* <Warning> : Grammar is replaced by Notation *)
-    Notation inc := (plus 1). 
+    Notation inc := (plus 1).
   End N.
 
   Definition zero := N.idid 0.
diff --git a/test-suite/modules/subtyping.v b/test-suite/modules/subtyping.v
index 2df8e84e5..dd7daf429 100644
--- a/test-suite/modules/subtyping.v
+++ b/test-suite/modules/subtyping.v
@@ -15,7 +15,7 @@ Module Type T.
 
  Parameter A : Type (* Top.1 *) .
 
- Inductive L : Type (* max(Top.1,1) *) := 
+ Inductive L : Type (* max(Top.1,1) *) :=
  | L0
  | L1 :  (A -> Prop) -> L.
 
@@ -23,17 +23,17 @@ End T.
 
 Axiom Tp : Type (* Top.5 *) .
 
-Module TT : T. 
+Module TT : T.
 
  Definition A : Type (* Top.6 *) := Tp. (* generates Top.5 <= Top.6 *)
 
- Inductive L : Type (* max(Top.6,1) *) := 
+ Inductive L : Type (* max(Top.6,1) *) :=
  | L0
  | L1 :  (A -> Prop) -> L.
 
 End TT. (* Generates Top.6 <= Top.1 (+ auxiliary constraints for L_rect) *)
 
-(* Note: Top.6 <= Top.1 is generated by subtyping on A; 
+(* Note: Top.6 <= Top.1 is generated by subtyping on A;
    subtyping of L follows and has not to be checked *)