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

5 files changed, 74 insertions, 74 deletions

diff --git a/theories/Sorting/Heap.v b/theories/Sorting/Heap.v
index 2d639d096..6d5564ed7 100644
--- a/theories/Sorting/Heap.v
+++ b/theories/Sorting/Heap.v
@@ -25,7 +25,7 @@ Section defs.
   Variable eqA : relation A.
 
   Let gtA (x y:A) := ~ leA x y.
-  
+
   Hypothesis leA_dec : forall x y:A, {leA x y} + {leA y x}.
   Hypothesis eqA_dec : forall x y:A, {eqA x y} + {~ eqA x y}.
   Hypothesis leA_refl : forall x y:A, eqA x y -> leA x y.
@@ -37,7 +37,7 @@ Section defs.
 
   Let emptyBag := EmptyBag A.
   Let singletonBag := SingletonBag _ eqA_dec.
-  
+
   Inductive Tree :=
     | Tree_Leaf : Tree
     | Tree_Node : A -> Tree -> Tree -> Tree.
@@ -92,7 +92,7 @@ Section defs.
       forall T:Tree, is_heap T -> P T.
   Proof.
     simple induction T; auto with datatypes.
-    intros a G PG D PD PN. 
+    intros a G PG D PD PN.
     elim (invert_heap a G D); auto with datatypes.
     intros H1 H2; elim H2; intros H3 H4; elim H4; intros.
     apply X0; auto with datatypes.
@@ -109,7 +109,7 @@ Section defs.
       forall T:Tree, is_heap T -> P T.
   Proof.
     simple induction T; auto with datatypes.
-    intros a G PG D PD PN. 
+    intros a G PG D PD PN.
     elim (invert_heap a G D); auto with datatypes.
     intros H1 H2; elim H2; intros H3 H4; elim H4; intros.
     apply X; auto with datatypes.
@@ -167,15 +167,15 @@ Section defs.
     elim (X a0); intros.
     apply insert_exist with (Tree_Node a T2 T0);
       auto using node_is_heap, nil_is_heap, leA_Tree_Leaf with datatypes.
-    simpl in |- *; apply treesort_twist1; trivial with datatypes. 
+    simpl in |- *; apply treesort_twist1; trivial with datatypes.
     elim (X a); intros T3 HeapT3 ConT3 LeA.
-    apply insert_exist with (Tree_Node a0 T2 T3); 
+    apply insert_exist with (Tree_Node a0 T2 T3);
       auto using node_is_heap, nil_is_heap, leA_Tree_Leaf with datatypes.
     apply node_is_heap; auto using node_is_heap, nil_is_heap, leA_Tree_Leaf with datatypes.
-    apply low_trans with a; auto with datatypes. 
+    apply low_trans with a; auto with datatypes.
     apply LeA; auto with datatypes.
     apply low_trans with a; auto with datatypes.
-    simpl in |- *; apply treesort_twist2; trivial with datatypes. 
+    simpl in |- *; apply treesort_twist2; trivial with datatypes.
   Qed.
 
 
@@ -186,7 +186,7 @@ Section defs.
     forall T:Tree,
       is_heap T ->
       meq (list_contents _ eqA_dec l) (contents T) -> build_heap l.
-  
+
   Lemma list_to_heap : forall l:list A, build_heap l.
   Proof.
     simple induction l.
@@ -204,7 +204,7 @@ Section defs.
 
 
   (** ** Building the sorted list *)
-  
+
   Inductive flat_spec (T:Tree) : Type :=
     flat_exist :
     forall l:list A,
diff --git a/theories/Sorting/PermutEq.v b/theories/Sorting/PermutEq.v
index f7bd37ee2..9bfe31ed1 100644
--- a/theories/Sorting/PermutEq.v
+++ b/theories/Sorting/PermutEq.v
@@ -13,22 +13,22 @@ Require Import Omega Relations Setoid List Multiset Permutation.
 Set Implicit Arguments.
 
 (** This file is similar to [PermutSetoid], except that the equality used here
-    is Coq usual one instead of a setoid equality. In particular, we can then 
-    prove the equivalence between [List.Permutation] and 
+    is Coq usual one instead of a setoid equality. In particular, we can then
+    prove the equivalence between [List.Permutation] and
     [Permutation.permutation].
 *)
 
 Section Perm.
-  
+
   Variable A : Type.
   Hypothesis eq_dec : forall x y:A, {x=y} + {~ x=y}.
-  
+
   Notation permutation := (permutation _ eq_dec).
   Notation list_contents := (list_contents _ eq_dec).
 
   (** we can use [multiplicity] to define [In] and [NoDup]. *)
 
-  Lemma multiplicity_In : 
+  Lemma multiplicity_In :
     forall l a, In a l <-> 0 < multiplicity (list_contents l) a.
   Proof.
     induction l.
@@ -49,18 +49,18 @@ Section Perm.
   Lemma multiplicity_In_O :
     forall l a, ~ In a l -> multiplicity (list_contents l) a = 0.
   Proof.
-    intros l a; rewrite multiplicity_In; 
+    intros l a; rewrite multiplicity_In;
       destruct (multiplicity (list_contents l) a); auto.
     destruct 1; auto with arith.
   Qed.
-  
+
   Lemma multiplicity_In_S :
     forall l a, In a l -> multiplicity (list_contents l) a >= 1.
   Proof.
     intros l a; rewrite multiplicity_In; auto.
   Qed.
 
-  Lemma multiplicity_NoDup : 
+  Lemma multiplicity_NoDup :
     forall l, NoDup l <-> (forall a, multiplicity (list_contents l) a <= 1).
   Proof.
     induction l.
@@ -78,7 +78,7 @@ Section Perm.
     generalize (H a).
     destruct (eq_dec a a) as [H0|H0].
     destruct (multiplicity (list_contents l) a); auto with arith.
-    simpl; inversion 1. 
+    simpl; inversion 1.
     inversion H3.
     destruct H0; auto.
     rewrite IHl; intros.
@@ -86,13 +86,13 @@ Section Perm.
     destruct (eq_dec a a0); simpl; auto with arith.
   Qed.
 
-  Lemma NoDup_permut : 
-    forall l l', NoDup l -> NoDup l' -> 
+  Lemma NoDup_permut :
+    forall l l', NoDup l -> NoDup l' ->
       (forall x, In x l <-> In x l') -> permutation l l'.
   Proof.
     intros.
     red; unfold meq; intros.
-    rewrite multiplicity_NoDup in H, H0. 
+    rewrite multiplicity_NoDup in H, H0.
     generalize (H a) (H0 a) (H1 a); clear H H0 H1.
     do 2 rewrite multiplicity_In.
     destruct 3; omega.
@@ -128,11 +128,11 @@ Section Perm.
     intro Abs; generalize (permut_In_In _ Abs H).
     inversion 1.
   Qed.
-  
-  (** When used with [eq], this permutation notion is equivalent to 
+
+  (** When used with [eq], this permutation notion is equivalent to
       the one defined in [List.v]. *)
 
-  Lemma permutation_Permutation : 
+  Lemma permutation_Permutation :
     forall l l', Permutation l l' <-> permutation l l'.
   Proof.
     split.
@@ -165,7 +165,7 @@ Section Perm.
     destruct (eq_dec b b) as [H|H]; [ | destruct H; auto].
     destruct (eq_dec a b); simpl; auto; intros; discriminate.
   Qed.
-  
+
   Lemma permut_length_2 :
     forall a1 b1 a2 b2, permutation (a1 :: b1 :: nil) (a2 :: b2 :: nil) ->
       (a1=a2) /\ (b1=b2) \/ (a1=b2) /\ (a2=b1).
@@ -177,7 +177,7 @@ Section Perm.
     apply permut_length_1.
     red; red; intros.
     generalize (P a); clear P; simpl.
-    destruct (eq_dec a1 a) as [H2|H2]; 
+    destruct (eq_dec a1 a) as [H2|H2];
       destruct (eq_dec a2 a) as [H3|H3]; auto.
     destruct H3; transitivity a1; auto.
     destruct H2; transitivity a2; auto.
@@ -187,7 +187,7 @@ Section Perm.
     apply permut_length_1.
     red; red; intros.
     generalize (P a); clear P; simpl.
-    destruct (eq_dec a1 a) as [H2|H2]; 
+    destruct (eq_dec a1 a) as [H2|H2];
       destruct (eq_dec b2 a) as [H3|H3]; auto.
     simpl; rewrite <- plus_n_Sm; inversion 1; auto.
     destruct H3; transitivity a1; auto.
@@ -210,12 +210,12 @@ Section Perm.
   Qed.
 
   Variable B : Type.
-  Variable eqB_dec : forall x y:B, { x=y }+{ ~x=y }. 
+  Variable eqB_dec : forall x y:B, { x=y }+{ ~x=y }.
 
   (** Permutation is compatible with map. *)
 
   Lemma permutation_map :
-    forall f l1 l2, permutation l1 l2 -> 
+    forall f l1 l2, permutation l1 l2 ->
       Permutation.permutation _ eqB_dec (map f l1) (map f l2).
   Proof.
     intros f; induction l1.
diff --git a/theories/Sorting/PermutSetoid.v b/theories/Sorting/PermutSetoid.v
index 1ea71972b..803a6143f 100644
--- a/theories/Sorting/PermutSetoid.v
+++ b/theories/Sorting/PermutSetoid.v
@@ -12,8 +12,8 @@ Require Import Omega Relations Multiset Permutation SetoidList.
 
 Set Implicit Arguments.
 
-(** This file contains additional results about permutations 
-     with respect to a setoid equality (i.e. an equivalence relation). 
+(** This file contains additional results about permutations
+     with respect to a setoid equality (i.e. an equivalence relation).
 *)
 
 Section Perm.
@@ -33,7 +33,7 @@ Variable eqA_trans : forall x y z, eqA x y -> eqA y z -> eqA x z.
 
 (** we can use [multiplicity] to define [InA] and [NoDupA]. *)
 
-Lemma multiplicity_InA : 
+Lemma multiplicity_InA :
   forall l a, InA eqA a l <-> 0 < multiplicity (list_contents l) a.
 Proof.
   induction l.
@@ -54,7 +54,7 @@ Qed.
 Lemma multiplicity_InA_O :
   forall l a, ~ InA eqA a l -> multiplicity (list_contents l) a = 0.
 Proof.
-  intros l a; rewrite multiplicity_InA; 
+  intros l a; rewrite multiplicity_InA;
     destruct (multiplicity (list_contents l) a); auto with arith.
   destruct 1; auto with arith.
 Qed.
@@ -65,7 +65,7 @@ Proof.
   intros l a; rewrite multiplicity_InA; auto with arith.
 Qed.
 
-Lemma multiplicity_NoDupA : forall l, 
+Lemma multiplicity_NoDupA : forall l,
   NoDupA eqA l <-> (forall a, multiplicity (list_contents l) a <= 1).
 Proof.
   induction l.
@@ -83,7 +83,7 @@ Proof.
   generalize (H a).
   destruct (eqA_dec a a) as [H0|H0].
   destruct (multiplicity (list_contents l) a); auto with arith.
-  simpl; inversion 1. 
+  simpl; inversion 1.
   inversion H3.
   destruct H0; auto.
   rewrite IHl; intros.
@@ -140,7 +140,7 @@ Proof.
   apply permut_length_1.
   red; red; intros.
   generalize (P a); clear P; simpl.
-  destruct (eqA_dec a1 a) as [H2|H2]; 
+  destruct (eqA_dec a1 a) as [H2|H2];
     destruct (eqA_dec a2 a) as [H3|H3]; auto.
   destruct H3; apply eqA_trans with a1; auto.
   destruct H2; apply eqA_trans with a2; auto.
@@ -150,7 +150,7 @@ Proof.
   apply permut_length_1.
   red; red; intros.
   generalize (P a); clear P; simpl.
-  destruct (eqA_dec a1 a) as [H2|H2]; 
+  destruct (eqA_dec a1 a) as [H2|H2];
     destruct (eqA_dec b2 a) as [H3|H3]; auto.
   simpl; rewrite <- plus_n_Sm; inversion 1; auto.
   destruct H3; apply eqA_trans with a1; auto.
@@ -174,19 +174,19 @@ Proof.
   apply permut_tran with (a::l1); auto.
   revert H1; unfold Permutation.permutation, meq; simpl.
   intros; f_equal; auto.
-  destruct (eqA_dec b a0) as [H2|H2]; 
+  destruct (eqA_dec b a0) as [H2|H2];
     destruct (eqA_dec a a0) as [H3|H3]; auto.
   destruct H3; apply eqA_trans with b; auto.
   destruct H2; apply eqA_trans with a; auto.
 Qed.
 
-Lemma NoDupA_equivlistA_permut : 
-  forall l l', NoDupA eqA l -> NoDupA eqA l' -> 
+Lemma NoDupA_equivlistA_permut :
+  forall l l', NoDupA eqA l -> NoDupA eqA l' ->
     equivlistA eqA l l' -> permutation l l'.
 Proof.
   intros.
   red; unfold meq; intros.
-  rewrite multiplicity_NoDupA in H, H0. 
+  rewrite multiplicity_NoDupA in H, H0.
   generalize (H a) (H0 a) (H1 a); clear H H0 H1.
   do 2 rewrite multiplicity_InA.
   destruct 3; omega.
@@ -195,15 +195,15 @@ Qed.
 
 Variable B : Type.
 Variable eqB : B->B->Prop.
-Variable eqB_dec : forall x y:B, { eqB x y }+{ ~eqB x y }. 
+Variable eqB_dec : forall x y:B, { eqB x y }+{ ~eqB x y }.
 Variable eqB_trans : forall x y z, eqB x y -> eqB y z -> eqB x z.
 
 (** Permutation is compatible with map. *)
 
 Lemma permut_map :
-  forall f, 
+  forall f,
     (forall x y, eqA x y -> eqB (f x) (f y)) ->
-    forall l1 l2, permutation l1 l2 -> 
+    forall l1 l2, permutation l1 l2 ->
       Permutation.permutation _ eqB_dec (map f l1) (map f l2).
 Proof.
   intros f; induction l1.
@@ -218,7 +218,7 @@ Proof.
   apply permut_tran with (f b :: map f l1).
   revert H1; unfold Permutation.permutation, meq; simpl.
   intros; f_equal; auto.
-  destruct (eqB_dec (f b) a0) as [H2|H2]; 
+  destruct (eqB_dec (f b) a0) as [H2|H2];
     destruct (eqB_dec (f a) a0) as [H3|H3]; auto.
   destruct H3; apply eqB_trans with (f b); auto.
   destruct H2; apply eqB_trans with (f a); auto.
@@ -229,7 +229,7 @@ Proof.
   apply permut_tran with (a::l1); auto.
   revert H1; unfold Permutation.permutation, meq; simpl.
   intros; f_equal; auto.
-  destruct (eqA_dec b a0) as [H2|H2]; 
+  destruct (eqA_dec b a0) as [H2|H2];
     destruct (eqA_dec a a0) as [H3|H3]; auto.
   destruct H3; apply eqA_trans with b; auto.
   destruct H2; apply eqA_trans with a; auto.
diff --git a/theories/Sorting/Permutation.v b/theories/Sorting/Permutation.v
index a92212054..9daf71b2b 100644
--- a/theories/Sorting/Permutation.v
+++ b/theories/Sorting/Permutation.v
@@ -10,9 +10,9 @@
 
 Require Import Relations List Multiset Arith.
 
-(** This file define a notion of permutation for lists, based on multisets: 
-    there exists a permutation between two lists iff every elements have 
-    the same multiplicity in the two lists. 
+(** This file define a notion of permutation for lists, based on multisets:
+    there exists a permutation between two lists iff every elements have
+    the same multiplicity in the two lists.
 
     Unlike [List.Permutation], the present notion of permutation
     requires the domain to be equipped with a decidable equality. This
@@ -22,10 +22,10 @@ Require Import Relations List Multiset Arith.
     The present file contains basic results, obtained without any particular
     assumption on the decidable equality used.
 
-    File [PermutSetoid] contains additional results about permutations 
-    with respect to an setoid equality (i.e. an equivalence relation). 
+    File [PermutSetoid] contains additional results about permutations
+    with respect to an setoid equality (i.e. an equivalence relation).
 
-    Finally, file [PermutEq] concerns Coq equality : this file is similar 
+    Finally, file [PermutEq] concerns Coq equality : this file is similar
     to the previous one, but proves in addition that [List.Permutation]
     and [permutation] are equivalent in this context.
 *)
@@ -62,9 +62,9 @@ Section defs.
       auto with datatypes.
   Qed.
 
-  
+
   (** * [permutation]: definition and basic properties *)
-  
+
   Definition permutation (l m:list A) :=
     meq (list_contents l) (list_contents m).
 
@@ -72,42 +72,42 @@ Section defs.
   Proof.
     unfold permutation in |- *; auto with datatypes.
   Qed.
-  
+
   Lemma permut_sym :
     forall l1 l2 : list A, permutation l1 l2 -> permutation l2 l1.
   Proof.
     unfold permutation, meq; intros; apply sym_eq; trivial.
   Qed.
-  
+
   Lemma permut_tran :
     forall l m n:list A, permutation l m -> permutation m n -> permutation l n.
   Proof.
     unfold permutation in |- *; intros.
     apply meq_trans with (list_contents m); auto with datatypes.
   Qed.
-  
+
   Lemma permut_cons :
     forall l m:list A,
       permutation l m -> forall a:A, permutation (a :: l) (a :: m).
   Proof.
     unfold permutation in |- *; simpl in |- *; auto with datatypes.
   Qed.
-  
+
   Lemma permut_app :
     forall l l' m m':list A,
       permutation l l' -> permutation m m' -> permutation (l ++ m) (l' ++ m').
   Proof.
     unfold permutation in |- *; intros.
-    apply meq_trans with (munion (list_contents l) (list_contents m)); 
+    apply meq_trans with (munion (list_contents l) (list_contents m));
       auto using permut_cons, list_contents_app with datatypes.
-    apply meq_trans with (munion (list_contents l') (list_contents m')); 
+    apply meq_trans with (munion (list_contents l') (list_contents m'));
       auto using permut_cons, list_contents_app with datatypes.
     apply meq_trans with (munion (list_contents l') (list_contents m));
       auto using permut_cons, list_contents_app with datatypes.
   Qed.
 
   Lemma permut_add_inside :
-    forall a l1 l2 l3 l4, 
+    forall a l1 l2 l3 l4,
       permutation (l1 ++ l2) (l3 ++ l4) ->
       permutation (l1 ++ a :: l2) (l3 ++ a :: l4).
   Proof.
@@ -118,9 +118,9 @@ Section defs.
     destruct (eqA_dec a a0); simpl; auto with arith.
     do 2 rewrite <- plus_n_Sm; f_equal; auto.
   Qed.
-  
+
   Lemma permut_add_cons_inside :
-    forall a l l1 l2, 
+    forall a l l1 l2,
       permutation l (l1 ++ l2) ->
       permutation (a :: l) (l1 ++ a :: l2).
   Proof.
@@ -134,17 +134,17 @@ Section defs.
   Proof.
     intros; apply permut_add_cons_inside; auto using permut_sym, permut_refl.
   Qed.
-  
+
   Lemma permut_sym_app :
     forall l1 l2, permutation (l1 ++ l2) (l2 ++ l1).
   Proof.
     intros l1 l2;
-      unfold permutation, meq; 
-	intro a; do 2 rewrite list_contents_app; simpl; 
+      unfold permutation, meq;
+	intro a; do 2 rewrite list_contents_app; simpl;
 	  auto with arith.
   Qed.
 
-  Lemma permut_rev : 
+  Lemma permut_rev :
     forall l, permutation l (rev l).
   Proof.
     induction l.
@@ -162,7 +162,7 @@ Section defs.
       generalize (H a); apply plus_reg_l.
   Qed.
 
-  Lemma permut_app_inv1 : 
+  Lemma permut_app_inv1 :
     forall l l1 l2, permutation (l1 ++ l) (l2 ++ l) -> permutation l1 l2.
   Proof.
     intros l l1 l2; unfold permutation, meq; simpl;
@@ -174,7 +174,7 @@ Section defs.
     trivial.
   Qed.
 
-  Lemma permut_app_inv2 : 
+  Lemma permut_app_inv2 :
     forall l l1 l2, permutation (l ++ l1) (l ++ l2) -> permutation l1 l2.
   Proof.
     intros l l1 l2; unfold permutation, meq; simpl;
@@ -186,7 +186,7 @@ Section defs.
   Qed.
 
   Lemma permut_remove_hd :
-    forall l l1 l2 a,   
+    forall l l1 l2 a,
       permutation (a :: l) (l1 ++ a :: l2) -> permutation l (l1 ++ l2).
   Proof.
     intros l l1 l2 a; unfold permutation, meq; simpl; intros H a0; generalize (H a0); clear H.
@@ -200,6 +200,6 @@ Section defs.
 
 End defs.
 
-(** For compatibilty *) 
+(** For compatibilty *)
 Notation permut_right := permut_cons.
 Unset Implicit Arguments.
diff --git a/theories/Sorting/Sorting.v b/theories/Sorting/Sorting.v
index 4c8173172..2d76b25a2 100644
--- a/theories/Sorting/Sorting.v
+++ b/theories/Sorting/Sorting.v
@@ -19,7 +19,7 @@ Section defs.
   Variable eqA : relation A.
 
   Let gtA (x y:A) := ~ leA x y.
-  
+
   Hypothesis leA_dec : forall x y:A, {leA x y} + {leA y x}.
   Hypothesis eqA_dec : forall x y:A, {eqA x y} + {~ eqA x y}.
   Hypothesis leA_refl : forall x y:A, eqA x y -> leA x y.
@@ -112,7 +112,7 @@ Section defs.
 
     (* 2 (leA a0 a) *)
     elim X0; simpl in |- *; intros.
-    apply merge_exist with (a0 :: l3); simpl in |- *; 
+    apply merge_exist with (a0 :: l3); simpl in |- *;
       auto using cons_sort, cons_leA with datatypes.
     apply meq_trans with
       (munion (singletonBag a0)