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

diff --git a/theories/Logic/Classical_Prop.v b/theories/Logic/Classical_Prop.v
index 8d2e946de..df732959f 100644
--- a/theories/Logic/Classical_Prop.v
+++ b/theories/Logic/Classical_Prop.v
@@ -22,7 +22,7 @@ unfold not in |- *; intros; elim (classic p); auto.
 intro NP; elim (H NP).
 Qed.
 
-(** Peirce's law states [forall P Q:Prop, ((P -> Q) -> P) -> P]. 
+(** Peirce's law states [forall P Q:Prop, ((P -> Q) -> P) -> P].
     Thanks to [forall P, False -> P], it is equivalent to the
     following form *)
 
@@ -95,11 +95,11 @@ Proof proof_irrelevance_cci classic.
 (* classical_left  transforms |- A \/ B into ~B |- A *)
 (* classical_right transforms |- A \/ B into ~A |- B *)
 
-Ltac classical_right :=  match goal with 
+Ltac classical_right :=  match goal with
  | _:_ |-?X1 \/ _ => (elim (classic X1);intro;[left;trivial|right])
 end.
 
-Ltac classical_left := match goal with 
+Ltac classical_left := match goal with
 | _:_ |- _ \/?X1 => (elim (classic X1);intro;[right;trivial|left])
 end.
 
@@ -107,7 +107,7 @@ Require Export EqdepFacts.
 
 Module Eq_rect_eq.
 
-Lemma eq_rect_eq : 
+Lemma eq_rect_eq :
   forall (U:Type) (p:U) (Q:U -> Type) (x:Q p) (h:p = p), x = eq_rect p Q x p h.
 Proof.
 intros; rewrite proof_irrelevance with (p1:=h) (p2:=refl_equal p); reflexivity.