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, 10 insertions, 8 deletions

diff --git a/theories/Bool/DecBool.v b/theories/Bool/DecBool.v
index 82363fff7..90f7ee662 100644
--- a/theories/Bool/DecBool.v
+++ b/theories/Bool/DecBool.v
@@ -15,17 +15,19 @@ Definition ifdec (A B:Prop) (C:Type) (H:{A} + {B}) (x y:C) : C :=
 
 
 Theorem ifdec_left :
- forall (A B:Prop) (C:Set) (H:{A} + {B}),
-   ~ B -> forall x y:C, ifdec H x y = x.
-intros; case H; auto.
-intro; absurd B; trivial.
+  forall (A B:Prop) (C:Set) (H:{A} + {B}),
+    ~ B -> forall x y:C, ifdec H x y = x.
+Proof.
+  intros; case H; auto.
+  intro; absurd B; trivial.
 Qed.
 
 Theorem ifdec_right :
- forall (A B:Prop) (C:Set) (H:{A} + {B}),
-   ~ A -> forall x y:C, ifdec H x y = y.
-intros; case H; auto.
-intro; absurd A; trivial.
+  forall (A B:Prop) (C:Set) (H:{A} + {B}),
+    ~ A -> forall x y:C, ifdec H x y = y.
+Proof.
+  intros; case H; auto.
+  intro; absurd A; trivial.
 Qed.
 
 Unset Implicit Arguments.