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

11 files changed, 39 insertions, 39 deletions

diff --git a/theories/Arith/Between.v b/theories/Arith/Between.v
index 3f96d4341..208c25789 100644
--- a/theories/Arith/Between.v
+++ b/theories/Arith/Between.v
@@ -17,11 +17,11 @@ Implicit Types k l p q r : nat.
 
 Section Between.
   Variables P Q : nat -> Prop.
-  
+
   Inductive between k : nat -> Prop :=
     | bet_emp : between k k
     | bet_S : forall l, between k l -> P l -> between k (S l).
-  
+
   Hint Constructors between: arith v62.
 
   Lemma bet_eq : forall k l, l = k -> between k l.
@@ -185,5 +185,5 @@ Section Between.
 End Between.
 
 Hint Resolve nth_O bet_S bet_emp bet_eq between_Sk_l exists_S exists_le
-  in_int_S in_int_intro: arith v62. 
+  in_int_S in_int_intro: arith v62.
 Hint Immediate in_int_Sp_q exists_le_S exists_S_le: arith v62.
diff --git a/theories/Arith/Compare_dec.v b/theories/Arith/Compare_dec.v
index 573f54e9f..a684d5a10 100644
--- a/theories/Arith/Compare_dec.v
+++ b/theories/Arith/Compare_dec.v
@@ -107,7 +107,7 @@ Qed.
 
 Theorem not_lt : forall n m, ~ n < m -> n >= m.
 Proof.
-  intros x y H; exact (not_gt y x H). 
+  intros x y H; exact (not_gt y x H).
 Qed.
 
 
diff --git a/theories/Arith/Div2.v b/theories/Arith/Div2.v
index 4c3b2ff84..999a64544 100644
--- a/theories/Arith/Div2.v
+++ b/theories/Arith/Div2.v
@@ -36,7 +36,7 @@ Proof.
   intros P H0 H1 Hn.
   cut (forall n, P n /\ P (S n)).
   intros H'n n. elim (H'n n). auto with arith.
-  
+
   induction n. auto with arith.
   intros. elim IHn; auto with arith.
 Qed.
@@ -150,7 +150,7 @@ Proof fun n => proj2 (proj2 (even_odd_double n)).
 
 Hint Resolve even_double double_even odd_double double_odd: arith.
 
-(** Application: 
+(** Application:
     - if [n] is even then there is a [p] such that [n = 2p]
     - if [n] is odd  then there is a [p] such that [n = 2p+1]
 
diff --git a/theories/Arith/Even.v b/theories/Arith/Even.v
index d2a4006a0..eaa1bb2d6 100644
--- a/theories/Arith/Even.v
+++ b/theories/Arith/Even.v
@@ -17,7 +17,7 @@ Open Local Scope nat_scope.
 Implicit Types m n : nat.
 
 
-(** * Definition of [even] and [odd], and basic facts *) 
+(** * Definition of [even] and [odd], and basic facts *)
 
 Inductive even : nat -> Prop :=
   | even_O : even 0
@@ -52,9 +52,9 @@ Qed.
 
 (** * Facts about [even] & [odd] wrt. [plus] *)
 
-Lemma even_plus_split : forall n m, 
+Lemma even_plus_split : forall n m,
   (even (n + m) -> even n /\ even m \/ odd n /\ odd m)
-with odd_plus_split : forall n m, 
+with odd_plus_split : forall n m,
   odd (n + m) -> odd n /\ even m \/ even n /\ odd m.
 Proof.
 intros. clear even_plus_split. destruct n; simpl in *.
@@ -95,7 +95,7 @@ Proof.
   intros n m H; destruct (even_plus_split n m) as [[]|[]]; auto.
   intro; destruct (not_even_and_odd n); auto.
 Qed.
- 
+
 Lemma even_plus_even_inv_l : forall n m, even (n + m) -> even m -> even n.
 Proof.
   intros n m H; destruct (even_plus_split n m) as [[]|[]]; auto.
@@ -120,13 +120,13 @@ Proof.
   intros n m H; destruct (odd_plus_split n m) as [[]|[]]; auto.
   intro; destruct (not_even_and_odd m); auto.
 Qed.
- 
+
 Lemma odd_plus_even_inv_r : forall n m, odd (n + m) -> odd n -> even m.
 Proof.
   intros n m H; destruct (odd_plus_split n m) as [[]|[]]; auto.
   intro; destruct (not_even_and_odd n); auto.
 Qed.
- 
+
 Lemma odd_plus_odd_inv_l : forall n m, odd (n + m) -> even m -> odd n.
 Proof.
   intros n m H; destruct (odd_plus_split n m) as [[]|[]]; auto.
@@ -203,7 +203,7 @@ Proof.
   intros n m; case (even_mult_aux n m); auto.
   intros H H0; case H0; auto.
 Qed.
- 
+
 Lemma even_mult_r : forall n m, even m -> even (n * m).
 Proof.
   intros n m; case (even_mult_aux n m); auto.
@@ -219,7 +219,7 @@ Proof.
   intros H'3; elim H'3; auto.
   intros H; case (not_even_and_odd n); auto.
 Qed.
- 
+
 Lemma even_mult_inv_l : forall n m, even (n * m) -> odd m -> even n.
 Proof.
   intros n m H' H'0.
@@ -228,13 +228,13 @@ Proof.
   intros H'3; elim H'3; auto.
   intros H; case (not_even_and_odd m); auto.
 Qed.
- 
+
 Lemma odd_mult : forall n m, odd n -> odd m -> odd (n * m).
 Proof.
   intros n m; case (even_mult_aux n m); intros H; case H; auto.
 Qed.
 Hint Resolve even_mult_l even_mult_r odd_mult: arith.
- 
+
 Lemma odd_mult_inv_l : forall n m, odd (n * m) -> odd n.
 Proof.
   intros n m H'.
diff --git a/theories/Arith/Lt.v b/theories/Arith/Lt.v
index 5d6e231c5..1fb5b3e55 100644
--- a/theories/Arith/Lt.v
+++ b/theories/Arith/Lt.v
@@ -26,7 +26,7 @@ Theorem lt_irrefl : forall n, ~ n < n.
 Proof le_Sn_n.
 Hint Resolve lt_irrefl: arith v62.
 
-(** * Relationship between [le] and [lt] *) 
+(** * Relationship between [le] and [lt] *)
 
 Theorem lt_le_S : forall n m, n < m -> S n <= m.
 Proof.
diff --git a/theories/Arith/Max.v b/theories/Arith/Max.v
index e43b804e5..dcc973a96 100644
--- a/theories/Arith/Max.v
+++ b/theories/Arith/Max.v
@@ -25,7 +25,7 @@ Fixpoint max n m {struct n} : nat :=
 
 (** * Inductive characterization of [max] *)
 
-Lemma max_case_strong : forall n m (P:nat -> Type), 
+Lemma max_case_strong : forall n m (P:nat -> Type),
   (m<=n -> P n) -> (n<=m -> P m) -> P (max n m).
 Proof.
   induction n; destruct m; simpl in *; auto with arith.
@@ -63,7 +63,7 @@ Qed.
 
 Lemma plus_max_distr_l : forall n m p, max (p + n) (p + m) = p + max n m.
 Proof.
-  induction p; simpl; auto. 
+  induction p; simpl; auto.
 Qed.
 
 Lemma plus_max_distr_r : forall n m p, max (n + p) (m + p) = max n m + p.
diff --git a/theories/Arith/Min.v b/theories/Arith/Min.v
index 7654c856c..503029015 100644
--- a/theories/Arith/Min.v
+++ b/theories/Arith/Min.v
@@ -27,7 +27,7 @@ Fixpoint min n m {struct n} : nat :=
 
 Lemma min_0_l : forall n : nat, min 0 n = 0.
 Proof.
-  trivial. 
+  trivial.
 Qed.
 
 Lemma min_0_r : forall n : nat, min n 0 = 0.
diff --git a/theories/Arith/Minus.v b/theories/Arith/Minus.v
index 1bf6102e9..b6ea04c01 100644
--- a/theories/Arith/Minus.v
+++ b/theories/Arith/Minus.v
@@ -120,10 +120,10 @@ Proof.
 
     intros n m Hnm; apply le_elim_rel with (n:=n) (m:=m); trivial.
       intros q; destruct q; auto with arith.
-        simpl. 
+        simpl.
         apply le_trans with (m := p - 0); [apply HI | rewrite <- minus_n_O];
           auto with arith.
-        
+
       intros q r Hqr _. simpl. auto using HI.
 Qed.
 
diff --git a/theories/Arith/Mult.v b/theories/Arith/Mult.v
index 1183dc2ee..7b48ffe05 100644
--- a/theories/Arith/Mult.v
+++ b/theories/Arith/Mult.v
@@ -43,7 +43,7 @@ Hint Resolve mult_1_l: arith v62.
 
 Lemma mult_1_r : forall n, n * 1 = n.
 Proof.
-  induction n; [ trivial | 
+  induction n; [ trivial |
     simpl; rewrite IHn; reflexivity].
 Qed.
 Hint Resolve mult_1_r: arith v62.
@@ -118,7 +118,7 @@ Proof.
     edestruct O_S; eauto.
     destruct plus_is_one with (1:=H) as [[-> Hnm] | [-> Hnm]].
       simpl in H; rewrite mult_0_r in H; elim (O_S _ H).
-      rewrite mult_1_r in Hnm; auto. 
+      rewrite mult_1_r in Hnm; auto.
 Qed.
 
 (** ** Multiplication and successor *)
@@ -176,7 +176,7 @@ Qed.
 
 Lemma mult_S_lt_compat_l : forall n m p, m < p -> S n * m < S n * p.
 Proof.
-  induction n; intros; simpl in *. 
+  induction n; intros; simpl in *.
     rewrite <- 2! plus_n_O; assumption.
     auto using plus_lt_compat.
 Qed.
@@ -219,8 +219,8 @@ Qed.
 
 (** * Tail-recursive mult *)
 
-(** [tail_mult] is an alternative definition for [mult] which is 
-    tail-recursive, whereas [mult] is not. This can be useful 
+(** [tail_mult] is an alternative definition for [mult] which is
+    tail-recursive, whereas [mult] is not. This can be useful
     when extracting programs. *)
 
 Fixpoint mult_acc (s:nat) m n {struct n} : nat :=
@@ -244,7 +244,7 @@ Proof.
   intros; unfold tail_mult in |- *; rewrite <- mult_acc_aux; auto.
 Qed.
 
-(** [TailSimpl] transforms any [tail_plus] and [tail_mult] into [plus] 
+(** [TailSimpl] transforms any [tail_plus] and [tail_mult] into [plus]
     and [mult] and simplify *)
 
 Ltac tail_simpl :=
diff --git a/theories/Arith/Plus.v b/theories/Arith/Plus.v
index 5f7517c75..cba87f9e5 100644
--- a/theories/Arith/Plus.v
+++ b/theories/Arith/Plus.v
@@ -65,7 +65,7 @@ Qed.
 Hint Resolve plus_assoc: arith v62.
 
 Lemma plus_permute : forall n m p, n + (m + p) = m + (n + p).
-Proof. 
+Proof.
   intros; rewrite (plus_assoc m n p); rewrite (plus_comm m n); auto with arith.
 Qed.
 
@@ -179,7 +179,7 @@ Definition plus_is_one :
 Proof.
   intro m; destruct m as [| n]; auto.
   destruct n; auto.
-  intros. 
+  intros.
   simpl in H. discriminate H.
 Defined.
 
@@ -187,14 +187,14 @@ Defined.
 
 Lemma plus_permute_2_in_4 : forall n m p q, n + m + (p + q) = n + p + (m + q).
 Proof.
-  intros m n p q. 
+  intros m n p q.
   rewrite <- (plus_assoc m n (p + q)). rewrite (plus_assoc n p q).
   rewrite (plus_comm n p). rewrite <- (plus_assoc p n q). apply plus_assoc.
 Qed.
 
 (** * Tail-recursive plus *)
 
-(** [tail_plus] is an alternative definition for [plus] which is 
+(** [tail_plus] is an alternative definition for [plus] which is
     tail-recursive, whereas [plus] is not. This can be useful
     when extracting programs. *)
 
@@ -215,7 +215,7 @@ Lemma succ_plus_discr : forall n m, n <> S (plus m n).
 Proof.
   intros n m; induction n as [|n IHn].
   discriminate.
-  intro H; apply IHn; apply eq_add_S; rewrite H; rewrite <- plus_n_Sm; 
+  intro H; apply IHn; apply eq_add_S; rewrite H; rewrite <- plus_n_Sm;
     reflexivity.
 Qed.
 
diff --git a/theories/Arith/Wf_nat.v b/theories/Arith/Wf_nat.v
index e87901080..d142cb77f 100644
--- a/theories/Arith/Wf_nat.v
+++ b/theories/Arith/Wf_nat.v
@@ -46,9 +46,9 @@ Defined.
 (** It is possible to directly prove the induction principle going
    back to primitive recursion on natural numbers ([induction_ltof1])
    or to use the previous lemmas to extract a program with a fixpoint
-   ([induction_ltof2]) 
+   ([induction_ltof2])
 
-the ML-like program for [induction_ltof1] is : 
+the ML-like program for [induction_ltof1] is :
 [[
 let induction_ltof1 f F a =
   let rec indrec n k =
@@ -58,7 +58,7 @@ let induction_ltof1 f F a =
   in indrec (f a + 1) a
 ]]
 
-the ML-like program for [induction_ltof2] is : 
+the ML-like program for [induction_ltof2] is :
 [[
    let induction_ltof2 F a = indrec a
    where rec indrec a = F a indrec;;
@@ -78,7 +78,7 @@ Proof.
   unfold ltof in |- *; intros b ltfafb.
   apply IHn.
   apply lt_le_trans with (f a); auto with arith.
-Defined. 
+Defined.
 
 Theorem induction_gtof1 :
   forall P:A -> Set,
@@ -271,8 +271,8 @@ Fixpoint iter_nat (n:nat) (A:Type) (f:A -> A) (x:A) {struct n} : A :=
 Theorem iter_nat_plus :
   forall (n m:nat) (A:Type) (f:A -> A) (x:A),
     iter_nat (n + m) A f x = iter_nat n A f (iter_nat m A f x).
-Proof.    
+Proof.
   simple induction n;
     [ simpl in |- *; auto with arith
-      | intros; simpl in |- *; apply f_equal with (f := f); apply H ].  
+      | intros; simpl in |- *; apply f_equal with (f := f); apply H ].
 Qed.