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

3 files changed, 42 insertions, 42 deletions

diff --git a/theories/Relations/Operators_Properties.v b/theories/Relations/Operators_Properties.v
index 2ced22298..d35841e00 100644
--- a/theories/Relations/Operators_Properties.v
+++ b/theories/Relations/Operators_Properties.v
@@ -24,7 +24,7 @@ Section Properties.
   Variable R : relation A.
 
   Let incl (R1 R2:relation A) : Prop := forall x y:A, R1 x y -> R2 x y.
-  
+
   Section Clos_Refl_Trans.
 
     (** Correctness of the reflexive-transitive closure operator *)
@@ -33,7 +33,7 @@ Section Properties.
     Proof.
       apply Build_preorder.
       exact (rt_refl A R).
-      
+
       exact (rt_trans A R).
     Qed.
 
@@ -114,7 +114,7 @@ Section Properties.
       apply t1n_trans; auto.
     Qed.
 
-    Lemma t1n_trans_equiv : forall x y, 
+    Lemma t1n_trans_equiv : forall x y,
         clos_trans A R x y <-> clos_trans_1n A R x y.
     Proof.
       split.
@@ -144,7 +144,7 @@ Section Properties.
       right with y0; auto.
     Qed.
 
-    Lemma tn1_trans_equiv : forall x y, 
+    Lemma tn1_trans_equiv : forall x y,
         clos_trans A R x y <-> clos_trans_n1 A R x y.
     Proof.
       split.
@@ -152,7 +152,7 @@ Section Properties.
       apply tn1_trans.
     Qed.
 
-    (** Direct reflexive-transitive closure is equivalent to 
+    (** Direct reflexive-transitive closure is equivalent to
         transitivity by left-step extension *)
 
     Lemma R_rt1n : forall x y, R x y -> clos_refl_trans_1n A R x y.
@@ -167,7 +167,7 @@ Section Properties.
       right with x;[assumption|left].
     Qed.
 
-    Lemma rt1n_trans : forall x y, 
+    Lemma rt1n_trans : forall x y,
         clos_refl_trans_1n A R x y -> clos_refl_trans A R x y.
     Proof.
       induction 1.
@@ -176,7 +176,7 @@ Section Properties.
       constructor 1; auto.
     Qed.
 
-    Lemma trans_rt1n : forall x y, 
+    Lemma trans_rt1n : forall x y,
         clos_refl_trans A R x y -> clos_refl_trans_1n A R x y.
     Proof.
       induction 1.
@@ -190,7 +190,7 @@ Section Properties.
       apply rt1n_trans; auto.
     Qed.
 
-    Lemma rt1n_trans_equiv : forall x y, 
+    Lemma rt1n_trans_equiv : forall x y,
       clos_refl_trans A R x y <-> clos_refl_trans_1n A R x y.
     Proof.
       split.
@@ -198,7 +198,7 @@ Section Properties.
       apply rt1n_trans.
     Qed.
 
-    (** Direct reflexive-transitive closure is equivalent to 
+    (** Direct reflexive-transitive closure is equivalent to
         transitivity by right-step extension *)
 
     Lemma rtn1_trans : forall x y,
@@ -210,7 +210,7 @@ Section Properties.
       constructor 1; assumption.
     Qed.
 
-    Lemma trans_rtn1 :  forall x y, 
+    Lemma trans_rtn1 :  forall x y,
         clos_refl_trans A R x y -> clos_refl_trans_n1 A R x y.
     Proof.
       induction 1.
@@ -221,7 +221,7 @@ Section Properties.
       right with y0; auto.
     Qed.
 
-    Lemma rtn1_trans_equiv : forall x y, 
+    Lemma rtn1_trans_equiv : forall x y,
         clos_refl_trans A R x y <-> clos_refl_trans_n1 A R x y.
     Proof.
       split.
@@ -240,7 +240,7 @@ Section Properties.
       revert H H0.
       induction H1; intros; auto with sets.
       apply H1 with x; auto with sets.
-      
+
       apply IHclos_refl_trans2.
       apply IHclos_refl_trans1; auto with sets.
 
@@ -270,10 +270,10 @@ Section Properties.
       eauto.
     Qed.
 
-    (** Direct reflexive-symmetric-transitive closure is equivalent to 
+    (** Direct reflexive-symmetric-transitive closure is equivalent to
         transitivity by symmetric left-step extension *)
 
-    Lemma rts1n_rts  : forall x y, 
+    Lemma rts1n_rts  : forall x y,
       clos_refl_sym_trans_1n A R x y -> clos_refl_sym_trans A R x y.
     Proof.
       induction 1.
@@ -283,7 +283,7 @@ Section Properties.
     Qed.
 
     Lemma rts_1n_trans : forall x y, clos_refl_sym_trans_1n A R x y ->
-      forall z, clos_refl_sym_trans_1n A R y z -> 
+      forall z, clos_refl_sym_trans_1n A R y z ->
         clos_refl_sym_trans_1n A R x z.
       induction 1.
       auto.
@@ -301,7 +301,7 @@ Section Properties.
       left.
     Qed.
 
-    Lemma rts_rts1n  : forall x y, 
+    Lemma rts_rts1n  : forall x y,
       clos_refl_sym_trans A R x y -> clos_refl_sym_trans_1n A R x y.
       induction 1.
       constructor 2 with y; auto.
@@ -311,7 +311,7 @@ Section Properties.
       eapply rts_1n_trans; eauto.
     Qed.
 
-    Lemma rts_rts1n_equiv : forall x y, 
+    Lemma rts_rts1n_equiv : forall x y,
       clos_refl_sym_trans A R x y <-> clos_refl_sym_trans_1n A R x y.
     Proof.
       split.
@@ -319,10 +319,10 @@ Section Properties.
       apply rts1n_rts.
     Qed.
 
-    (** Direct reflexive-symmetric-transitive closure is equivalent to 
+    (** Direct reflexive-symmetric-transitive closure is equivalent to
         transitivity by symmetric right-step extension *)
 
-    Lemma rtsn1_rts : forall x y, 
+    Lemma rtsn1_rts : forall x y,
       clos_refl_sym_trans_n1 A R x y -> clos_refl_sym_trans A R x y.
     Proof.
       induction 1.
@@ -332,7 +332,7 @@ Section Properties.
     Qed.
 
     Lemma rtsn1_trans : forall y z, clos_refl_sym_trans_n1 A R y z->
-      forall x, clos_refl_sym_trans_n1 A R x y -> 
+      forall x, clos_refl_sym_trans_n1 A R x y ->
         clos_refl_sym_trans_n1 A R x z.
     Proof.
       induction 1.
@@ -352,7 +352,7 @@ Section Properties.
       left.
     Qed.
 
-    Lemma rts_rtsn1 : forall x y, 
+    Lemma rts_rtsn1 : forall x y,
       clos_refl_sym_trans A R x y -> clos_refl_sym_trans_n1 A R x y.
     Proof.
       induction 1.
@@ -363,7 +363,7 @@ Section Properties.
       eapply rtsn1_trans; eauto.
     Qed.
 
-    Lemma rts_rtsn1_equiv : forall x y, 
+    Lemma rts_rtsn1_equiv : forall x y,
       clos_refl_sym_trans A R x y <-> clos_refl_sym_trans_n1 A R x y.
     Proof.
       split.
diff --git a/theories/Relations/Relation_Definitions.v b/theories/Relations/Relation_Definitions.v
index 977135fab..c03c4b95f 100644
--- a/theories/Relations/Relation_Definitions.v
+++ b/theories/Relations/Relation_Definitions.v
@@ -11,14 +11,14 @@
 Section Relation_Definition.
 
   Variable A : Type.
-  
+
   Definition relation := A -> A -> Prop.
 
   Variable R : relation.
-   
+
 
   Section General_Properties_of_Relations.
-    
+
     Definition reflexive : Prop := forall x:A, R x x.
     Definition transitive : Prop := forall x y z:A, R x y -> R y z -> R x z.
     Definition symmetric : Prop := forall x y:A, R x y -> R y x.
@@ -32,33 +32,33 @@ Section Relation_Definition.
 
 
   Section Sets_of_Relations.
-    
-    Record preorder : Prop := 
+
+    Record preorder : Prop :=
       { preord_refl : reflexive; preord_trans : transitive}.
-    
-    Record order : Prop := 
+
+    Record order : Prop :=
       { ord_refl : reflexive;
 	ord_trans : transitive;
 	ord_antisym : antisymmetric}.
-    
-    Record equivalence : Prop := 
+
+    Record equivalence : Prop :=
       { equiv_refl : reflexive;
 	equiv_trans : transitive;
 	equiv_sym : symmetric}.
-    
+
     Record PER : Prop :=  {per_sym : symmetric; per_trans : transitive}.
 
   End Sets_of_Relations.
 
 
   Section Relations_of_Relations.
-    
+
     Definition inclusion (R1 R2:relation) : Prop :=
       forall x y:A, R1 x y -> R2 x y.
-    
+
     Definition same_relation (R1 R2:relation) : Prop :=
       inclusion R1 R2 /\ inclusion R2 R1.
-    
+
     Definition commut (R1 R2:relation) : Prop :=
       forall x y:A,
 	R1 y x -> forall z:A, R2 z y ->  exists2 y' : A, R2 y' x & R1 z y'.
diff --git a/theories/Relations/Relation_Operators.v b/theories/Relations/Relation_Operators.v
index eec3f8ebd..2d1503f23 100644
--- a/theories/Relations/Relation_Operators.v
+++ b/theories/Relations/Relation_Operators.v
@@ -65,7 +65,7 @@ Section Reflexive_Transitive_Closure.
 
   Inductive clos_refl_trans_1n (x: A) : A -> Prop :=
     | rt1n_refl : clos_refl_trans_1n x x
-    | rt1n_trans (y z:A) : 
+    | rt1n_trans (y z:A) :
          R x y -> clos_refl_trans_1n y z -> clos_refl_trans_1n x z.
 
   (** Alternative definition by transitive extension on the right *)
@@ -82,7 +82,7 @@ End Reflexive_Transitive_Closure.
 Section Reflexive_Symetric_Transitive_Closure.
   Variable A : Type.
   Variable R : relation A.
-  
+
   (** Definition by direct reflexive-symmetric-transitive closure *)
 
   Inductive clos_refl_sym_trans : relation A :=
@@ -104,7 +104,7 @@ Section Reflexive_Symetric_Transitive_Closure.
 
   Inductive clos_refl_sym_trans_n1 (x: A) : A -> Prop :=
     | rtsn1_refl : clos_refl_sym_trans_n1 x x
-    | rtsn1_trans (y z:A) : R y z \/ R z y -> 
+    | rtsn1_trans (y z:A) : R y z \/ R z y ->
          clos_refl_sym_trans_n1 x y -> clos_refl_sym_trans_n1 x z.
 
 End Reflexive_Symetric_Transitive_Closure.
@@ -139,7 +139,7 @@ Inductive le_AsB : A + B -> A + B -> Prop :=
   | le_ab (x:A) (y:B) : le_AsB (inl _ x) (inr _ y)
   | le_bb (x y:B) : leB x y -> le_AsB (inr _ x) (inr _ y).
 
-End Disjoint_Union. 
+End Disjoint_Union.
 
 (** ** Lexicographic order on dependent pairs *)
 
@@ -189,12 +189,12 @@ End Swap.
 
 
 Section Lexicographic_Exponentiation.
-  
+
   Variable A : Set.
   Variable leA : A -> A -> Prop.
   Let Nil := nil (A:=A).
   Let List := list A.
-  
+
   Inductive Ltl : List -> List -> Prop :=
     | Lt_nil (a:A) (x:List) : Ltl Nil (a :: x)
     | Lt_hd (a b:A) : leA a b -> forall x y:list A, Ltl (a :: x) (b :: y)
@@ -207,7 +207,7 @@ Section Lexicographic_Exponentiation.
         leA x y -> Desc (l ++ y :: Nil) -> Desc ((l ++ y :: Nil) ++ x :: Nil).
 
   Definition Pow : Set := sig Desc.
-  
+
   Definition lex_exp (a b:Pow) : Prop := Ltl (proj1_sig a) (proj1_sig b).
 
 End Lexicographic_Exponentiation.