Mise en forme des theories

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9245 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 17 insertions, 17 deletions

diff --git a/theories/Logic/ClassicalEpsilon.v b/theories/Logic/ClassicalEpsilon.v
index 6c8631a9b..102edba5d 100644
--- a/theories/Logic/ClassicalEpsilon.v
+++ b/theories/Logic/ClassicalEpsilon.v
@@ -8,7 +8,7 @@
 
 (*i $Id$ i*)
 
-(** *** This file provides classical logic and indefinite description
+(** This file provides classical logic and indefinite description
     (Hilbert's epsilon operator) *)
 
 (** Classical epsilon's operator (i.e. indefinite description) implies
@@ -23,28 +23,28 @@ Set Implicit Arguments.
 
 Axiom constructive_indefinite_description :
   forall (A : Type) (P : A->Prop), 
-  (exists x, P x) -> { x : A | P x }.
+    (exists x, P x) -> { x : A | P x }.
 
 Lemma constructive_definite_description :
   forall (A : Type) (P : A->Prop), 
-  (exists! x, P x) -> { x : A | P x }.
+    (exists! x, P x) -> { x : A | P x }.
 Proof.
-intros; apply constructive_indefinite_description; firstorder.
+  intros; apply constructive_indefinite_description; firstorder.
 Qed.
 
 Theorem excluded_middle_informative : forall P:Prop, {P} + {~ P}.
 Proof.
-apply 
-  (constructive_definite_descr_excluded_middle 
-   constructive_definite_description classic).
+  apply 
+    (constructive_definite_descr_excluded_middle 
+      constructive_definite_description classic).
 Qed.
 
 Theorem classical_indefinite_description : 
   forall (A : Type) (P : A->Prop), inhabited A ->
-  { x : A | (exists x, P x) -> P x }.
+    { x : A | (exists x, P x) -> P x }.
 Proof.
-intros A P i.
-destruct (excluded_middle_informative (exists x, P x)) as [Hex|HnonP].
+  intros A P i.
+  destruct (excluded_middle_informative (exists x, P x)) as [Hex|HnonP].
   apply constructive_indefinite_description 
     with (P:= fun x => (exists x, P x) -> P x).
   destruct Hex as (x,Hx).
@@ -90,13 +90,13 @@ Opaque epsilon.
 (** *** Weaker lemmas (compatibility lemmas) *)
 
 Theorem choice :
- forall (A B : Type) (R : A->B->Prop),
-   (forall x : A, exists y : B, R x y) ->
-   (exists f : A->B, forall x : A, R x (f x)).
+  forall (A B : Type) (R : A->B->Prop),
+    (forall x : A, exists y : B, R x y) ->
+    (exists f : A->B, forall x : A, R x (f x)).
 Proof.
-intros A B R H.
-exists (fun x => proj1_sig (constructive_indefinite_description _ (H x))).
-intro x.
-apply (proj2_sig (constructive_indefinite_description _ (H x))).
+  intros A B R H.
+  exists (fun x => proj1_sig (constructive_indefinite_description _ (H x))).
+  intro x.
+  apply (proj2_sig (constructive_indefinite_description _ (H x))).
 Qed.