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

8 files changed, 68 insertions, 68 deletions

diff --git a/theories/Wellfounded/Disjoint_Union.v b/theories/Wellfounded/Disjoint_Union.v
index f6ce84f98..785d623b4 100644
--- a/theories/Wellfounded/Disjoint_Union.v
+++ b/theories/Wellfounded/Disjoint_Union.v
@@ -9,8 +9,8 @@
 (*i $Id$ i*)
 
 (** Author: Cristina Cornes
-    From : Constructing Recursion Operators in Type Theory                 
-           L. Paulson  JSC (1986) 2, 325-355 *) 
+    From : Constructing Recursion Operators in Type Theory
+           L. Paulson  JSC (1986) 2, 325-355 *)
 
 Require Import Relation_Operators.
 
@@ -20,7 +20,7 @@ Section Wf_Disjoint_Union.
   Variable leB : B -> B -> Prop.
 
   Notation Le_AsB := (le_AsB A B leA leB).
-  
+
   Lemma acc_A_sum : forall x:A, Acc leA x -> Acc Le_AsB (inl B x).
   Proof.
     induction 1.
@@ -47,7 +47,7 @@ Section Wf_Disjoint_Union.
     destruct a as [a| b].
     apply (acc_A_sum a).
     apply (H a).
-    
+
     apply (acc_B_sum H b).
     apply (H0 b).
   Qed.
diff --git a/theories/Wellfounded/Inclusion.v b/theories/Wellfounded/Inclusion.v
index e72b1e11d..01049989e 100644
--- a/theories/Wellfounded/Inclusion.v
+++ b/theories/Wellfounded/Inclusion.v
@@ -21,7 +21,7 @@ Section WfInclusion.
     induction 2.
     apply Acc_intro; auto with sets.
   Qed.
-  
+
   Hint Resolve Acc_incl.
 
   Theorem wf_incl : inclusion A R1 R2 -> well_founded R2 -> well_founded R1.
diff --git a/theories/Wellfounded/Inverse_Image.v b/theories/Wellfounded/Inverse_Image.v
index df6a61198..c57e70725 100644
--- a/theories/Wellfounded/Inverse_Image.v
+++ b/theories/Wellfounded/Inverse_Image.v
@@ -47,8 +47,8 @@ Section Inverse_Image.
     destruct H3.
     apply (IHAcc x1); auto.
   Qed.
-  
-  
+
+
   Theorem wf_inverse_rel : well_founded R -> well_founded RoF.
   Proof.
     red in |- *; constructor; intros.
diff --git a/theories/Wellfounded/Lexicographic_Exponentiation.v b/theories/Wellfounded/Lexicographic_Exponentiation.v
index 69421255d..ff1889000 100644
--- a/theories/Wellfounded/Lexicographic_Exponentiation.v
+++ b/theories/Wellfounded/Lexicographic_Exponentiation.v
@@ -10,7 +10,7 @@
 
 (** Author: Cristina Cornes
 
-    From : Constructing Recursion Operators in Type Theory                
+    From : Constructing Recursion Operators in Type Theory
            L. Paulson  JSC (1986) 2, 325-355  *)
 
 Require Import List.
@@ -20,12 +20,12 @@ Require Import Transitive_Closure.
 Section Wf_Lexicographic_Exponentiation.
   Variable A : Set.
   Variable leA : A -> A -> Prop.
-  
+
   Notation Power := (Pow A leA).
   Notation Lex_Exp := (lex_exp A leA).
   Notation ltl := (Ltl A leA).
   Notation Descl := (Desc A leA).
-  
+
   Notation List := (list A).
   Notation Nil := (nil (A:=A)).
   (* useless but symmetric *)
@@ -33,13 +33,13 @@ Section Wf_Lexicographic_Exponentiation.
   Notation "<< x , y >>" := (exist Descl x y) (at level 0, x, y at level 100).
 
   (* Hint Resolve d_one d_nil t_step. *)
-  
+
   Lemma left_prefix : forall x y z:List, ltl (x ++ y) z -> ltl x z.
   Proof.
     simple induction x.
     simple induction z.
     simpl in |- *; intros H.
-    inversion_clear H. 
+    inversion_clear H.
     simpl in |- *; intros; apply (Lt_nil A leA).
     intros a l HInd.
     simpl in |- *.
@@ -71,12 +71,12 @@ Section Wf_Lexicographic_Exponentiation.
     rewrite H8.
     right; exists x2; auto with sets.
   Qed.
-  
+
   Lemma desc_prefix : forall (x:List) (a:A), Descl (x ++ Cons a Nil) -> Descl x.
   Proof.
     intros.
     inversion H.
-    generalize (app_cons_not_nil _ _ _ H1); simple induction 1. 
+    generalize (app_cons_not_nil _ _ _ H1); simple induction 1.
     cut (x ++ Cons a Nil = Cons x0 Nil); auto with sets.
     intro.
     generalize (app_eq_unit _ _ H0).
@@ -87,7 +87,7 @@ Section Wf_Lexicographic_Exponentiation.
     simple induction 1; intros.
     rewrite <- H4; auto with sets.
   Qed.
-  
+
   Lemma desc_tail :
     forall (x:List) (a b:A),
       Descl (Cons b (x ++ Cons a Nil)) -> clos_trans A leA a b.
@@ -99,7 +99,7 @@ Section Wf_Lexicographic_Exponentiation.
         forall a b:A,
           Descl (Cons b (x ++ Cons a Nil)) -> clos_trans A leA a b).
     intros.
-    
+
     inversion H.
     cut (Cons b (Cons a Nil) = (Nil ++ Cons b Nil) ++ Cons a Nil);
       auto with sets; intro.
@@ -108,17 +108,17 @@ Section Wf_Lexicographic_Exponentiation.
     generalize (app_inj_tail (l ++ Cons y Nil) (Nil ++ Cons b Nil) _ _ H4);
       simple induction 1.
     intros.
-    
+
     generalize (app_inj_tail _ _ _ _ H6); simple induction 1; intros.
     generalize H1.
     rewrite <- H10; rewrite <- H7; intro.
     apply (t_step A leA); auto with sets.
-    
+
     intros.
     inversion H0.
     generalize (app_cons_not_nil _ _ _ H3); intro.
     elim H1.
-    
+
     generalize H0.
     generalize (app_comm_cons (l ++ Cons x0 Nil) (Cons a Nil) b);
       simple induction 1.
@@ -127,11 +127,11 @@ Section Wf_Lexicographic_Exponentiation.
     generalize (H x0 b H6).
     intro.
     apply t_trans with (A := A) (y := x0); auto with sets.
-    
+
     apply t_step.
     generalize H1.
     rewrite H4; intro.
-    
+
     generalize (app_inj_tail _ _ _ _ H8); simple induction 1.
     intros.
     generalize H2; generalize (app_comm_cons l (Cons x0 Nil) b).
@@ -154,7 +154,7 @@ Section Wf_Lexicographic_Exponentiation.
     generalize (app_eq_nil _ _ H0); simple induction 1.
     intros.
     rewrite H2; rewrite H3; split; apply d_nil.
-    
+
     intros.
     cut (x0 ++ y = Cons x Nil); auto with sets.
     intros E.
@@ -162,15 +162,15 @@ Section Wf_Lexicographic_Exponentiation.
     simple induction 1; intros.
     rewrite H2; rewrite H3; split.
     apply d_nil.
-    
+
     apply d_one.
-    
+
     simple induction 1; intros.
     rewrite H2; rewrite H3; split.
     apply d_one.
-    
+
     apply d_nil.
-    
+
     do 5 intro.
     intros Hind.
     do 2 intro.
@@ -181,13 +181,13 @@ Section Wf_Lexicographic_Exponentiation.
         forall x0:List,
           (l ++ Cons y Nil) ++ Cons x Nil = x0 ++ y0 ->
           Descl x0 /\ Descl y0).
-    
+
     intro.
     generalize (app_nil_end x1); simple induction 1; simple induction 1.
     split. apply d_conc; auto with sets.
-    
+
     apply d_nil.
-    
+
     do 3 intro.
     generalize x1.
     apply rev_ind with
@@ -202,7 +202,7 @@ Section Wf_Lexicographic_Exponentiation.
     split.
     generalize (app_inj_tail _ _ _ _ H2); simple induction 1.
     simple induction 1; auto with sets.
-    
+
     apply d_one.
     do 5 intro.
     generalize (app_ass x4 (l1 ++ Cons x2 Nil) (Cons x3 Nil)).
@@ -219,7 +219,7 @@ Section Wf_Lexicographic_Exponentiation.
     generalize (Hind x4 (l1 ++ Cons x2 Nil) H11).
     simple induction 1; split.
     auto with sets.
-    
+
     generalize H14.
     rewrite <- H10; intro.
     apply d_conc; auto with sets.
@@ -233,11 +233,11 @@ Section Wf_Lexicographic_Exponentiation.
     intros.
     apply (dist_aux (x ++ y) H x y); auto with sets.
   Qed.
-  
+
   Lemma desc_end :
     forall (a b:A) (x:List),
       Descl (x ++ Cons a Nil) /\ ltl (x ++ Cons a Nil) (Cons b Nil) ->
-      clos_trans A leA a b. 
+      clos_trans A leA a b.
   Proof.
     intros a b x.
     case x.
@@ -246,14 +246,14 @@ Section Wf_Lexicographic_Exponentiation.
     intros.
     inversion H1; auto with sets.
     inversion H3.
-    
+
     simple induction 1.
     generalize (app_comm_cons l (Cons a Nil) a0).
     intros E; rewrite <- E; intros.
     generalize (desc_tail l a a0 H0); intro.
     inversion H1.
     apply t_trans with (y := a0); auto with sets.
-    
+
     inversion H4.
   Qed.
 
@@ -268,15 +268,15 @@ Section Wf_Lexicographic_Exponentiation.
     intro.
     case x.
     intros; apply (Lt_nil A leA).
-    
+
     simpl in |- *; intros.
     inversion_clear H0.
     apply (Lt_hd A leA a b); auto with sets.
-    
+
     inversion_clear H1.
   Qed.
-  
-  
+
+
   Lemma acc_app :
     forall (x1 x2:List) (y1:Descl (x1 ++ x2)),
       Acc Lex_Exp << x1 ++ x2, y1 >> ->
@@ -285,11 +285,11 @@ Section Wf_Lexicographic_Exponentiation.
     intros.
     apply (Acc_inv (R:=Lex_Exp) (x:=<< x1 ++ x2, y1 >>)).
     auto with sets.
-    
+
     unfold lex_exp in |- *; simpl in |- *; auto with sets.
   Qed.
-  
-  
+
+
   Theorem wf_lex_exp : well_founded leA -> well_founded Lex_Exp.
   Proof.
     unfold well_founded at 2 in |- *.
@@ -303,7 +303,7 @@ Section Wf_Lexicographic_Exponentiation.
 	forall (x0:List) (y:Descl x0), ltl x0 x -> Acc Lex_Exp << x0, y >>).
     intros.
     inversion_clear H0.
-    
+
     intro.
     generalize (well_founded_ind (wf_clos_trans A leA H)).
     intros GR.
@@ -318,7 +318,7 @@ Section Wf_Lexicographic_Exponentiation.
     generalize (right_prefix x2 l (Cons x1 Nil) H1).
     simple induction 1.
     intro; apply (H0 x2 y1 H3).
-    
+
     simple induction 1.
     intro; simple induction 1.
     clear H4 H2.
@@ -340,8 +340,8 @@ Section Wf_Lexicographic_Exponentiation.
     unfold lex_exp at 1 in |- *.
     simpl in |- *; intros x4 y3. intros.
     apply (H0 x4 y3); auto with sets.
-    
-    intros. 
+
+    intros.
     generalize (dist_Desc_concat l (l0 ++ Cons x4 Nil) y1).
     simple induction 1.
     intros.
diff --git a/theories/Wellfounded/Lexicographic_Product.v b/theories/Wellfounded/Lexicographic_Product.v
index f41b6e93d..5144c0bee 100644
--- a/theories/Wellfounded/Lexicographic_Product.v
+++ b/theories/Wellfounded/Lexicographic_Product.v
@@ -14,7 +14,7 @@ Require Import Eqdep.
 Require Import Relation_Operators.
 Require Import Transitive_Closure.
 
-(**  From : Constructing Recursion Operators in Type Theory            
+(**  From : Constructing Recursion Operators in Type Theory
      L. Paulson  JSC (1986) 2, 325-355 *)
 
 Section WfLexicographic_Product.
@@ -24,7 +24,7 @@ Section WfLexicographic_Product.
   Variable leB : forall x:A, B x -> B x -> Prop.
 
   Notation LexProd := (lexprod A B leA leB).
-  
+
   Lemma acc_A_B_lexprod :
     forall x:A,
       Acc leA x ->
@@ -41,16 +41,16 @@ Section WfLexicographic_Product.
     intros.
     apply H2.
     apply t_trans with x2; auto with sets.
-    
+
     red in H2.
     apply H2.
     auto with sets.
-    
+
     injection H1.
     destruct 2.
     injection H3.
     destruct 2; auto with sets.
-    
+
     rewrite <- H1.
     injection H3; intros _ Hx1.
     subst x1.
@@ -105,7 +105,7 @@ End Wf_Symmetric_Product.
 
 
 Section Swap.
-  
+
   Variable A : Type.
   Variable R : A -> A -> Prop.
 
@@ -121,13 +121,13 @@ Section Swap.
     inversion_clear H; inversion_clear H1; apply H0.
     apply sp_swap.
     apply right_sym; auto with sets.
-    
+
     apply sp_swap.
     apply left_sym; auto with sets.
-    
+
     apply sp_noswap.
     apply right_sym; auto with sets.
-    
+
     apply sp_noswap.
     apply left_sym; auto with sets.
   Qed.
@@ -147,20 +147,20 @@ Section Swap.
     destruct y; intro H5.
     inversion_clear H5.
     inversion_clear H0; auto with sets.
-    
+
     apply swap_Acc.
     inversion_clear H0; auto with sets.
-    
+
     intros.
     apply IHAcc1; auto with sets; intros.
     apply Acc_inv with (y0, x1); auto with sets.
     apply sp_noswap.
     apply right_sym; auto with sets.
-    
+
     auto with sets.
   Qed.
 
-  
+
   Lemma wf_swapprod : well_founded R -> well_founded SwapProd.
   Proof.
     red in |- *.
diff --git a/theories/Wellfounded/Transitive_Closure.v b/theories/Wellfounded/Transitive_Closure.v
index 5e33da5ff..bce32af48 100644
--- a/theories/Wellfounded/Transitive_Closure.v
+++ b/theories/Wellfounded/Transitive_Closure.v
@@ -18,7 +18,7 @@ Section Wf_Transitive_Closure.
   Variable R : relation A.
 
   Notation trans_clos := (clos_trans A R).
- 
+
   Lemma incl_clos_trans : inclusion A R trans_clos.
     red in |- *; auto with sets.
   Qed.
diff --git a/theories/Wellfounded/Union.v b/theories/Wellfounded/Union.v
index ebf4ba98e..fbb3d9e3c 100644
--- a/theories/Wellfounded/Union.v
+++ b/theories/Wellfounded/Union.v
@@ -17,9 +17,9 @@ Require Import Transitive_Closure.
 Section WfUnion.
   Variable A : Type.
   Variables R1 R2 : relation A.
-  
+
   Notation Union := (union A R1 R2).
-  
+
   Remark strip_commut :
     commut A R1 R2 ->
     forall x y:A,
@@ -29,7 +29,7 @@ Section WfUnion.
     induction 2 as [x y| x y z H0 IH1 H1 IH2]; intros.
     elim H with y x z; auto with sets; intros x0 H2 H3.
     exists x0; auto with sets.
-    
+
     elim IH1 with z0; auto with sets; intros.
     elim IH2 with x0; auto with sets; intros.
     exists x1; auto with sets.
@@ -50,7 +50,7 @@ Section WfUnion.
     elim H8; intros.
     apply H6; auto with sets.
     apply t_trans with x0; auto with sets.
-    
+
     elim strip_commut with x x0 y0; auto with sets; intros.
     apply Acc_inv_trans with x1; auto with sets.
     unfold union in |- *.
@@ -63,7 +63,7 @@ Section WfUnion.
     apply Acc_intro; auto with sets.
   Qed.
 
-  
+
   Theorem wf_union :
     commut A R1 R2 -> well_founded R1 -> well_founded R2 -> well_founded Union.
   Proof.
diff --git a/theories/Wellfounded/Well_Ordering.v b/theories/Wellfounded/Well_Ordering.v
index 7296897ef..e11b89248 100644
--- a/theories/Wellfounded/Well_Ordering.v
+++ b/theories/Wellfounded/Well_Ordering.v
@@ -16,15 +16,15 @@ Require Import Eqdep.
 
 Section WellOrdering.
   Variable A : Type.
-  Variable B : A -> Type. 
-  
+  Variable B : A -> Type.
+
   Inductive WO : Type :=
     sup : forall (a:A) (f:B a -> WO), WO.
 
 
   Inductive le_WO : WO -> WO -> Prop :=
     le_sup : forall (a:A) (f:B a -> WO) (v:B a), le_WO (f v) (sup a f).
- 
+
   Theorem wf_WO : well_founded le_WO.
   Proof.
     unfold well_founded in |- *; intro.