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

diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v
index 147d1e8d34..8d790d1fd7 100644
--- a/theories/Init/Datatypes.v
+++ b/theories/Init/Datatypes.v
@@ -98,7 +98,7 @@ Defined.
 
 (** [nat] is the datatype of natural numbers built from [O] and successor [S];
     note that the constructor name is the letter O.
-    Numbers in [nat] can be denoted using a decimal notation; 
+    Numbers in [nat] can be denoted using a decimal notation;
     e.g. [3%nat] abbreviates [S (S (S O))] *)
 
 Inductive nat : Set :=
@@ -166,7 +166,7 @@ Section projections.
   Definition snd (p:A * B) := match p with
 				| (x, y) => y
                               end.
-End projections. 
+End projections.
 
 Hint Resolve pair inl inr: core.
 
@@ -181,13 +181,13 @@ Lemma injective_projections :
     fst p1 = fst p2 -> snd p1 = snd p2 -> p1 = p2.
 Proof.
   destruct p1; destruct p2; simpl in |- *; intros Hfst Hsnd.
-  rewrite Hfst; rewrite Hsnd; reflexivity. 
+  rewrite Hfst; rewrite Hsnd; reflexivity.
 Qed.
 
-Definition prod_uncurry (A B C:Type) (f:prod A B -> C) 
+Definition prod_uncurry (A B C:Type) (f:prod A B -> C)
   (x:A) (y:B) : C := f (pair x y).
 
-Definition prod_curry (A B C:Type) (f:A -> B -> C) 
+Definition prod_curry (A B C:Type) (f:A -> B -> C)
   (p:prod A B) : C := match p with
                        | pair x y => f x y
                        end.
diff --git a/theories/Init/Logic_Type.v b/theories/Init/Logic_Type.v
index bdec651da3..1333f3545e 100644
--- a/theories/Init/Logic_Type.v
+++ b/theories/Init/Logic_Type.v
@@ -28,7 +28,7 @@ Section identity_is_a_congruence.
  Variable f : A -> B.
 
  Variables x y z : A.
- 
+
  Lemma identity_sym : identity x y -> identity y x.
  Proof.
   destruct 1; trivial.
diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v
index 2244e1b9a9..748229b176 100644
--- a/theories/Init/Specif.v
+++ b/theories/Init/Specif.v
@@ -18,9 +18,9 @@ Require Import Logic.
 
 (** Subsets and Sigma-types *)
 
-(** [(sig A P)], or more suggestively [{x:A | P x}], denotes the subset 
+(** [(sig A P)], or more suggestively [{x:A | P x}], denotes the subset
     of elements of the type [A] which satisfy the predicate [P].
-    Similarly [(sig2 A P Q)], or [{x:A | P x & Q x}], denotes the subset 
+    Similarly [(sig2 A P Q)], or [{x:A | P x & Q x}], denotes the subset
     of elements of the type [A] which satisfy both [P] and [Q]. *)
 
 Inductive sig (A:Type) (P:A -> Prop) : Type :=
@@ -29,7 +29,7 @@ Inductive sig (A:Type) (P:A -> Prop) : Type :=
 Inductive sig2 (A:Type) (P Q:A -> Prop) : Type :=
     exist2 : forall x:A, P x -> Q x -> sig2 P Q.
 
-(** [(sigT A P)], or more suggestively [{x:A & (P x)}] is a Sigma-type. 
+(** [(sigT A P)], or more suggestively [{x:A & (P x)}] is a Sigma-type.
     Similarly for [(sigT2 A P Q)], also written [{x:A & (P x) & (Q x)}]. *)
 
 Inductive sigT (A:Type) (P:A -> Type) : Type :=
@@ -123,7 +123,7 @@ Coercion sig_of_sigT : sigT >-> sig.
 
 Inductive sumbool (A B:Prop) : Set :=
   | left : A -> {A} + {B}
-  | right : B -> {A} + {B} 
+  | right : B -> {A} + {B}
  where "{ A } + { B }" := (sumbool A B) : type_scope.
 
 Add Printing If sumbool.
@@ -133,7 +133,7 @@ Add Printing If sumbool.
 
 Inductive sumor (A:Type) (B:Prop) : Type :=
   | inleft : A -> A + {B}
-  | inright : B -> A + {B} 
+  | inright : B -> A + {B}
  where "A + { B }" := (sumor A B) : type_scope.
 
 Add Printing If sumor.
@@ -186,12 +186,12 @@ Section Choice_lemmas.
 
 End Choice_lemmas.
 
- (** A result of type [(Exc A)] is either a normal value of type [A] or 
+ (** A result of type [(Exc A)] is either a normal value of type [A] or
      an [error] :
 
      [Inductive Exc [A:Type] : Type := value : A->(Exc A) | error : (Exc A)].
 
-     It is implemented using the option type. *) 
+     It is implemented using the option type. *)
 
 Definition Exc := option.
 Definition value := Some.
diff --git a/theories/Init/Tactics.v b/theories/Init/Tactics.v
index 39cd268d9b..0d36d40e35 100644
--- a/theories/Init/Tactics.v
+++ b/theories/Init/Tactics.v
@@ -14,38 +14,38 @@ Require Import Specif.
 
 (** * Useful tactics *)
 
-(** A tactic for proof by contradiction. With contradict H, 
+(** A tactic for proof by contradiction. With contradict H,
     -   H:~A |-  B    gives       |-  A
     -   H:~A |- ~B    gives  H: B |-  A
     -   H: A |-  B    gives       |- ~A
     -   H: A |- ~B    gives  H: B |- ~A
     -   H:False leads to a resolved subgoal.
-   Moreover, negations may be in unfolded forms, 
+   Moreover, negations may be in unfolded forms,
    and A or B may live in Type *)
 
 Ltac contradict H :=
   let save tac H := let x:=fresh in intro x; tac H; rename x into H
-  in 
-  let negpos H := case H; clear H 
-  in 
+  in
+  let negpos H := case H; clear H
+  in
   let negneg H := save negpos H
   in
-  let pospos H := 
+  let pospos H :=
     let A := type of H in (elimtype False; revert H; try fold (~A))
   in
   let posneg H := save pospos H
-  in 
-  let neg H := match goal with 
+  in
+  let neg H := match goal with
    | |- (~_) => negneg H
    | |- (_->False) => negneg H
    | |- _ => negpos H
-  end in 
-  let pos H := match goal with 
+  end in
+  let pos H := match goal with
    | |- (~_) => posneg H
    | |- (_->False) => posneg H
    | |- _ => pospos H
   end in
-  match type of H with 
+  match type of H with
    | (~_) => neg H
    | (_->False) => neg H
    | _ => (elim H;fail) || pos H
@@ -53,20 +53,20 @@ Ltac contradict H :=
 
 (* Transforming a negative goal [ H:~A |- ~B ] into a positive one [ B |- A ]*)
 
-Ltac swap H := 
+Ltac swap H :=
   idtac "swap is OBSOLETE: use contradict instead.";
   intro; apply H; clear H.
 
 (* To contradict an hypothesis without copying its type. *)
 
-Ltac absurd_hyp H := 
+Ltac absurd_hyp H :=
   idtac "absurd_hyp is OBSOLETE: use contradict instead.";
-  let T := type of H in 
+  let T := type of H in
   absurd T.
 
 (* A useful complement to contradict. Here H:A while G allows to conclude ~A *)
 
-Ltac false_hyp H G := 
+Ltac false_hyp H G :=
   let T := type of H in absurd T; [ apply G | assumption ].
 
 (* A case with no loss of information. *)
@@ -77,11 +77,11 @@ Ltac case_eq x := generalize (refl_equal x); pattern x at -1; case x.
 
 Tactic Notation "destruct_with_eqn" constr(x) :=
   destruct x as []_eqn.
-Tactic Notation "destruct_with_eqn" ident(n) := 
+Tactic Notation "destruct_with_eqn" ident(n) :=
   try intros until n; destruct n as []_eqn.
 Tactic Notation "destruct_with_eqn" ":" ident(H) constr(x) :=
   destruct x as []_eqn:H.
-Tactic Notation "destruct_with_eqn" ":" ident(H) ident(n) := 
+Tactic Notation "destruct_with_eqn" ":" ident(H) ident(n) :=
   try intros until n; destruct n as []_eqn:H.
 
 (* Rewriting in all hypothesis several times everywhere *)
@@ -181,7 +181,7 @@ Ltac now_show c := change c.
 
 Set Implicit Arguments.
 
-Lemma decide_left : forall (C:Prop) (decide:{C}+{~C}), 
+Lemma decide_left : forall (C:Prop) (decide:{C}+{~C}),
   C -> forall P:{C}+{~C}->Prop, (forall H:C, P (left _ H)) -> P decide.
 Proof.
 intros; destruct decide. apply H0. contradiction.
@@ -194,8 +194,8 @@ intros; destruct decide. contradiction. apply H0.
 Qed.
 
 Tactic Notation "decide" constr(lemma) "with" constr(H) :=
-  let try_to_merge_hyps H := 
-     try (clear H; intro H) || 
+  let try_to_merge_hyps H :=
+     try (clear H; intro H) ||
      (let H' := fresh H "bis" in intro H'; try clear H') ||
      (let H' := fresh in intro H'; try clear H') in
   match type of H with
diff --git a/theories/Init/Wf.v b/theories/Init/Wf.v
index 2d35a4b237..f1baf71a7f 100644
--- a/theories/Init/Wf.v
+++ b/theories/Init/Wf.v
@@ -65,7 +65,7 @@ Section Well_founded.
   exact (fun P:A -> Prop => well_founded_induction_type P).
  Defined.
 
-(** Well-founded fixpoints *) 
+(** Well-founded fixpoints *)
 
  Section FixPoint.
 
@@ -80,13 +80,13 @@ Section Well_founded.
   Lemma Fix_F_eq :
    forall (x:A) (r:Acc x),
      F (fun (y:A) (p:R y x) => Fix_F (x:=y) (Acc_inv r p)) = Fix_F (x:=x) r.
-  Proof. 
+  Proof.
    destruct r using Acc_inv_dep; auto.
   Qed.
 
   Definition Fix (x:A) := Fix_F (Rwf x).
 
-  (** Proof that [well_founded_induction] satisfies the fixpoint equation. 
+  (** Proof that [well_founded_induction] satisfies the fixpoint equation.
       It requires an extra property of the functional *)
 
   Hypothesis
@@ -111,7 +111,7 @@ Section Well_founded.
 
  End FixPoint.
 
-End Well_founded. 
+End Well_founded.
 
 (** Well-founded fixpoints over pairs *)
 
@@ -120,7 +120,7 @@ Section Well_founded_2.
   Variables A B : Type.
   Variable R : A * B -> A * B -> Prop.
 
-  Variable P : A -> B -> Type. 
+  Variable P : A -> B -> Type.
 
   Section FixPoint_2.
 
@@ -129,7 +129,7 @@ Section Well_founded_2.
       forall (x:A) (x':B),
         (forall (y:A) (y':B), R (y, y') (x, x') -> P y y') -> P x x'.
 
-  Fixpoint Fix_F_2 (x:A) (x':B) (a:Acc R (x, x')) {struct a} : 
+  Fixpoint Fix_F_2 (x:A) (x':B) (a:Acc R (x, x')) {struct a} :
    P x x' :=
     F
       (fun (y:A) (y':B) (h:R (y, y') (x, x')) =>