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

1 files changed, 12 insertions, 12 deletions

diff --git a/theories/Logic/Eqdep_dec.v b/theories/Logic/Eqdep_dec.v
index 1943c1629..c7cb9b0d4 100644
--- a/theories/Logic/Eqdep_dec.v
+++ b/theories/Logic/Eqdep_dec.v
@@ -38,7 +38,7 @@ Set Implicit Arguments.
 Section EqdepDec.
 
   Variable A : Type.
-  
+
   Let comp (x y y':A) (eq1:x = y) (eq2:x = y') : y = y' :=
     eq_ind _ (fun a => a = y') eq2 _ eq1.
 
@@ -49,7 +49,7 @@ Section EqdepDec.
   Qed.
 
   Variable eq_dec : forall x y:A, x = y \/ x <> y.
-  
+
   Variable x : A.
 
   Let nu (y:A) (u:x = y) : x = y :=
@@ -63,13 +63,13 @@ Section EqdepDec.
     unfold nu in |- *.
     case (eq_dec x y); intros.
     reflexivity.
-  
+
     case n; trivial.
   Qed.
 
 
   Let nu_inv (y:A) (v:x = y) : x = y := comp (nu (refl_equal x)) v.
-  
+
 
   Remark nu_left_inv : forall (y:A) (u:x = y), nu_inv (nu u) = u.
   Proof.
@@ -88,7 +88,7 @@ Section EqdepDec.
     reflexivity.
   Qed.
 
-  Theorem K_dec : 
+  Theorem K_dec :
     forall P:x = x -> Prop, P (refl_equal x) -> forall p:x = x, P p.
   Proof.
     intros.
@@ -118,10 +118,10 @@ Section EqdepDec.
     case (eq_dec x x).
     intro e.
     elim e using K_dec; trivial.
-    
+
     intros.
     case n; trivial.
-    
+
     case H.
     reflexivity.
   Qed.
@@ -173,13 +173,13 @@ Unset Implicit Arguments.
 (** The signature of decidable sets in [Type] *)
 
 Module Type DecidableType.
-  
+
   Parameter U:Type.
   Axiom eq_dec : forall x y:U, {x = y} + {x <> y}.
 
 End DecidableType.
 
-(** The module [DecidableEqDep] collects equality properties for decidable 
+(** The module [DecidableEqDep] collects equality properties for decidable
     set in [Type] *)
 
 Module DecidableEqDep (M:DecidableType).
@@ -247,7 +247,7 @@ Module Type DecidableSet.
 
 End DecidableSet.
 
-(** The module [DecidableEqDepSet] collects equality properties for decidable 
+(** The module [DecidableEqDepSet] collects equality properties for decidable
     set in [Set] *)
 
 Module DecidableEqDepSet (M:DecidableSet).
@@ -307,11 +307,11 @@ End DecidableEqDepSet.
   (** From decidability to inj_pair2 **)
 Lemma inj_pair2_eq_dec : forall A:Type, (forall x y:A, {x=y}+{x<>y}) ->
    ( forall (P:A -> Type) (p:A) (x y:P p), existT P p x = existT P p y -> x = y ).
-Proof. 
+Proof.
   intros A eq_dec.
   apply eq_dep_eq__inj_pair2.
   apply eq_rect_eq__eq_dep_eq.
-  unfold Eq_rect_eq. 
+  unfold Eq_rect_eq.
   apply eq_rect_eq_dec.
   apply eq_dec.
 Qed.