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

diff --git a/theories/Classes/Morphisms_Prop.v b/theories/Classes/Morphisms_Prop.v
index b672651b9..5b61e2c07 100644
--- a/theories/Classes/Morphisms_Prop.v
+++ b/theories/Classes/Morphisms_Prop.v
@@ -7,7 +7,7 @@
 (************************************************************************)
 
 (* [Proper] instances for propositional connectives.
- 
+
    Author: Matthieu Sozeau
    Institution: LRI, CNRS UMR 8623 - Université Paris Sud
    91405 Orsay, France *)
@@ -25,7 +25,7 @@ Obligation Tactic := simpl_relation.
 Program Instance not_impl_morphism :
   Proper (impl --> impl) not | 1.
 
-Program Instance not_iff_morphism : 
+Program Instance not_iff_morphism :
   Proper (iff ++> iff) not.
 
 (** Logical conjunction. *)
@@ -33,15 +33,15 @@ Program Instance not_iff_morphism :
 Program Instance and_impl_morphism :
   Proper (impl ==> impl ==> impl) and | 1.
 
-Program Instance and_iff_morphism : 
+Program Instance and_iff_morphism :
   Proper (iff ==> iff ==> iff) and.
 
 (** Logical disjunction. *)
 
-Program Instance or_impl_morphism : 
+Program Instance or_impl_morphism :
   Proper (impl ==> impl ==> impl) or | 1.
 
-Program Instance or_iff_morphism : 
+Program Instance or_iff_morphism :
   Proper (iff ==> iff ==> iff) or.
 
 (** Logical implication [impl] is a morphism for logical equivalence. *)
@@ -54,11 +54,11 @@ Program Instance ex_iff_morphism {A : Type} : Proper (pointwise_relation A iff =
 
   Next Obligation.
   Proof.
-    unfold pointwise_relation in H.     
+    unfold pointwise_relation in H.
     split ; intros.
     destruct H0 as [x₁ H₁].
     exists x₁. rewrite H in H₁. assumption.
-    
+
     destruct H0 as [x₁ H₁].
     exists x₁. rewrite H. assumption.
   Qed.
@@ -68,20 +68,20 @@ Program Instance ex_impl_morphism {A : Type} :
 
   Next Obligation.
   Proof.
-    unfold pointwise_relation in H.  
+    unfold pointwise_relation in H.
     exists H0. apply H. assumption.
   Qed.
 
-Program Instance ex_inverse_impl_morphism {A : Type} : 
+Program Instance ex_inverse_impl_morphism {A : Type} :
   Proper (pointwise_relation A (inverse impl) ==> inverse impl) (@ex A) | 1.
 
   Next Obligation.
   Proof.
-    unfold pointwise_relation in H.  
+    unfold pointwise_relation in H.
     exists H0. apply H. assumption.
   Qed.
 
-Program Instance all_iff_morphism {A : Type} : 
+Program Instance all_iff_morphism {A : Type} :
   Proper (pointwise_relation A iff ==> iff) (@all A).
 
   Next Obligation.
@@ -90,18 +90,18 @@ Program Instance all_iff_morphism {A : Type} :
     intuition ; specialize (H x0) ; intuition.
   Qed.
 
-Program Instance all_impl_morphism {A : Type} : 
+Program Instance all_impl_morphism {A : Type} :
   Proper (pointwise_relation A impl ==> impl) (@all A) | 1.
-  
+
   Next Obligation.
   Proof.
     unfold pointwise_relation, all in *.
     intuition ; specialize (H x0) ; intuition.
   Qed.
 
-Program Instance all_inverse_impl_morphism {A : Type} : 
+Program Instance all_inverse_impl_morphism {A : Type} :
   Proper (pointwise_relation A (inverse impl) ==> inverse impl) (@all A) | 1.
-  
+
   Next Obligation.
   Proof.
     unfold pointwise_relation, all in *.