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

1 files changed, 20 insertions, 20 deletions

diff --git a/theories/Init/Tactics.v b/theories/Init/Tactics.v
index 39cd268d9..0d36d40e3 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