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

diff --git a/theories/Program/Wf.v b/theories/Program/Wf.v
index 041b318e8..9b7ea0474 100644
--- a/theories/Program/Wf.v
+++ b/theories/Program/Wf.v
@@ -22,20 +22,20 @@ Section Well_founded.
   Variable A : Type.
   Variable R : A -> A -> Prop.
   Hypothesis Rwf : well_founded R.
-    
+
   Variable P : A -> Type.
-  
+
   Variable F_sub : forall x:A, (forall y: { y : A | R y x }, P (proj1_sig y)) -> P x.
-  
+
   Fixpoint Fix_F_sub (x : A) (r : Acc R x) {struct r} : P x :=
-    F_sub x (fun y: { y : A | R y x}  => Fix_F_sub (proj1_sig y) 
+    F_sub x (fun y: { y : A | R y x}  => Fix_F_sub (proj1_sig y)
       (Acc_inv r (proj2_sig y))).
-  
+
   Definition Fix_sub (x : A) := Fix_F_sub x (Rwf x).
-  
-  (* Notation Fix_F := (Fix_F_sub P F_sub) (only parsing). (* alias *) *)  
+
+  (* Notation Fix_F := (Fix_F_sub P F_sub) (only parsing). (* alias *) *)
   (* Definition Fix (x:A) := Fix_F_sub P F_sub x (Rwf x). *)
-  
+
   Hypothesis
     F_ext :
     forall (x:A) (f g:forall y:{y:A | R y x}, P (`y)),
@@ -44,10 +44,10 @@ Section Well_founded.
   Lemma Fix_F_eq :
     forall (x:A) (r:Acc R x),
       F_sub x (fun (y:A|R y x) => Fix_F_sub (`y) (Acc_inv r (proj2_sig y))) = Fix_F_sub x r.
-  Proof. 
+  Proof.
     destruct r using Acc_inv_dep; auto.
   Qed.
-  
+
   Lemma Fix_F_inv : forall (x:A) (r s:Acc R x), Fix_F_sub x r = Fix_F_sub x s.
   Proof.
     intro x; induction (Rwf x); intros.
@@ -115,7 +115,7 @@ Section Fix_rects.
   Variable R : A -> A -> Prop.
   Variable Rwf : well_founded R.
   Variable f: forall (x : A), (forall y: { y: A | R y x }, P (proj1_sig y)) -> P x.
-  
+
   Lemma F_unfold x r:
     Fix_F_sub A R P f x r =
     f (fun y => Fix_F_sub A R P f (proj1_sig y) (Acc_inv r (proj2_sig y))).
@@ -200,8 +200,8 @@ Section Fix_rects.
     intros.
     assert (forall y: A, R y x0 -> Q y (Fix_F_sub A R P f y (Rwf y)))...
     set (inv x0 X0 a). clearbody q.
-    rewrite <- (equiv_lowers (fun y: {y: A | R y x0} => 
-      Fix_F_sub A R P f (proj1_sig y) (Rwf (proj1_sig y))) 
+    rewrite <- (equiv_lowers (fun y: {y: A | R y x0} =>
+      Fix_F_sub A R P f (proj1_sig y) (Rwf (proj1_sig y)))
     (fun y: {y: A | R y x0} => Fix_F_sub A R P f (proj1_sig y) (Acc_inv a (proj2_sig y))))...
     intros.
     apply eq_Fix_F_sub.
@@ -213,9 +213,9 @@ End Fix_rects.
 
 Ltac fold_sub f :=
   match goal with
-    | [ |- ?T ] => 
+    | [ |- ?T ] =>
       match T with
-        appcontext C [ @Fix_sub _ _ _ _ ?arg ] => 
+        appcontext C [ @Fix_sub _ _ _ _ ?arg ] =>
         let app := context C [ f arg ] in
           change app
       end
@@ -230,7 +230,7 @@ Module WfExtensionality.
 
   (** The two following lemmas allow to unfold a well-founded fixpoint definition without
      restriction using the functional extensionality axiom. *)
-  
+
   (** For a function defined with Program using a well-founded order. *)
 
   Program Lemma fix_sub_eq_ext :
@@ -247,11 +247,11 @@ Module WfExtensionality.
     extensionality y ; apply H.
     rewrite H0 ; auto.
   Qed.
-  
+
   (** Tactic to unfold once a definition based on [Fix_sub]. *)
-  
-  Ltac unfold_sub f fargs := 
-    set (call:=fargs) ; unfold f in call ; unfold call ; clear call ; 
+
+  Ltac unfold_sub f fargs :=
+    set (call:=fargs) ; unfold f in call ; unfold call ; clear call ;
       rewrite fix_sub_eq_ext ; repeat fold_sub fargs ; simpl proj1_sig.
 
 End WfExtensionality.