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

diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v
index 147d1e8d3..8d790d1fd 100644
--- a/theories/Init/Datatypes.v
+++ b/theories/Init/Datatypes.v
@@ -98,7 +98,7 @@ Defined.
 
 (** [nat] is the datatype of natural numbers built from [O] and successor [S];
     note that the constructor name is the letter O.
-    Numbers in [nat] can be denoted using a decimal notation; 
+    Numbers in [nat] can be denoted using a decimal notation;
     e.g. [3%nat] abbreviates [S (S (S O))] *)
 
 Inductive nat : Set :=
@@ -166,7 +166,7 @@ Section projections.
   Definition snd (p:A * B) := match p with
 				| (x, y) => y
                               end.
-End projections. 
+End projections.
 
 Hint Resolve pair inl inr: core.
 
@@ -181,13 +181,13 @@ Lemma injective_projections :
     fst p1 = fst p2 -> snd p1 = snd p2 -> p1 = p2.
 Proof.
   destruct p1; destruct p2; simpl in |- *; intros Hfst Hsnd.
-  rewrite Hfst; rewrite Hsnd; reflexivity. 
+  rewrite Hfst; rewrite Hsnd; reflexivity.
 Qed.
 
-Definition prod_uncurry (A B C:Type) (f:prod A B -> C) 
+Definition prod_uncurry (A B C:Type) (f:prod A B -> C)
   (x:A) (y:B) : C := f (pair x y).
 
-Definition prod_curry (A B C:Type) (f:A -> B -> C) 
+Definition prod_curry (A B C:Type) (f:A -> B -> C)
   (p:prod A B) : C := match p with
                        | pair x y => f x y
                        end.