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, 13 insertions, 13 deletions

diff --git a/theories/Logic/DecidableType.v b/theories/Logic/DecidableType.v
index fed25ad742..625f776bfa 100644
--- a/theories/Logic/DecidableType.v
+++ b/theories/Logic/DecidableType.v
@@ -14,7 +14,7 @@ Unset Strict Implicit.
 
 (** * Types with Equalities, and nothing more (for subtyping purpose) *)
 
-Module Type EqualityType. 
+Module Type EqualityType.
 
   Parameter Inline t : Type.
 
@@ -27,11 +27,11 @@ Module Type EqualityType.
   Hint Immediate eq_sym.
   Hint Resolve eq_refl eq_trans.
 
-End EqualityType. 
+End EqualityType.
 
 (** * Types with decidable Equalities (but no ordering) *)
 
-Module Type DecidableType. 
+Module Type DecidableType.
 
   Parameter Inline t : Type.
 
@@ -46,7 +46,7 @@ Module Type DecidableType.
   Hint Immediate eq_sym.
   Hint Resolve eq_refl eq_trans.
 
-End DecidableType. 
+End DecidableType.
 
 (** * Additional notions about keys and datas used in FMap *)
 
@@ -58,21 +58,21 @@ Module KeyDecidableType(D:DecidableType).
  Notation key:=t.
 
   Definition eqk (p p':key*elt) := eq (fst p) (fst p').
-  Definition eqke (p p':key*elt) := 
+  Definition eqke (p p':key*elt) :=
           eq (fst p) (fst p') /\ (snd p) = (snd p').
 
   Hint Unfold eqk eqke.
   Hint Extern 2 (eqke ?a ?b) => split.
 
    (* eqke is stricter than eqk *)
- 
+
    Lemma eqke_eqk : forall x x', eqke x x' -> eqk x x'.
    Proof.
      unfold eqk, eqke; intuition.
    Qed.
 
   (* eqk, eqke are equalities *)
- 
+
   Lemma eqk_refl : forall e, eqk e e.
   Proof. auto. Qed.
 
@@ -96,7 +96,7 @@ Module KeyDecidableType(D:DecidableType).
   Hint Resolve eqk_trans eqke_trans eqk_refl eqke_refl.
   Hint Immediate eqk_sym eqke_sym.
 
-  Lemma InA_eqke_eqk : 
+  Lemma InA_eqke_eqk :
      forall x m, InA eqke x m -> InA eqk x m.
   Proof.
     unfold eqke; induction 1; intuition.
@@ -134,22 +134,22 @@ Module KeyDecidableType(D:DecidableType).
   Lemma In_eq : forall l x y, eq x y -> In x l -> In y l.
   Proof.
   destruct 2 as (e,E); exists e; eapply MapsTo_eq; eauto.
-  Qed. 
+  Qed.
 
   Lemma In_inv : forall k k' e l, In k ((k',e) :: l) -> eq k k' \/ In k l.
   Proof.
     inversion 1.
     inversion_clear H0; eauto.
     destruct H1; simpl in *; intuition.
-  Qed.      
+  Qed.
 
-  Lemma In_inv_2 : forall k k' e e' l, 
+  Lemma In_inv_2 : forall k k' e e' l,
       InA eqk (k, e) ((k', e') :: l) -> ~ eq k k' -> InA eqk (k, e) l.
-  Proof.  
+  Proof.
    inversion_clear 1; compute in H0; intuition.
   Qed.
 
-  Lemma In_inv_3 : forall x x' l, 
+  Lemma In_inv_3 : forall x x' l,
       InA eqke x (x' :: l) -> ~ eqk x x' -> InA eqke x l.
   Proof.
    inversion_clear 1; compute in H0; intuition.