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, 6 deletions

diff --git a/theories/Bool/Zerob.v b/theories/Bool/Zerob.v
index eac13569a..5e9d4afa6 100644
--- a/theories/Bool/Zerob.v
+++ b/theories/Bool/Zerob.v
@@ -15,24 +15,28 @@ Open Local Scope nat_scope.
 
 Definition zerob (n:nat) : bool :=
   match n with
-  | O => true
-  | S _ => false
+    | O => true
+    | S _ => false
   end.
 
 Lemma zerob_true_intro : forall n:nat, n = 0 -> zerob n = true.
-destruct n; [ trivial with bool | inversion 1 ].
+Proof.
+  destruct n; [ trivial with bool | inversion 1 ].
 Qed.
 Hint Resolve zerob_true_intro: bool.
 
 Lemma zerob_true_elim : forall n:nat, zerob n = true -> n = 0.
-destruct n; [ trivial with bool | inversion 1 ].
+Proof.
+  destruct n; [ trivial with bool | inversion 1 ].
 Qed.
 
 Lemma zerob_false_intro : forall n:nat, n <> 0 -> zerob n = false.
-destruct n; [ destruct 1; auto with bool | trivial with bool ].
+Proof.
+  destruct n; [ destruct 1; auto with bool | trivial with bool ].
 Qed.
 Hint Resolve zerob_false_intro: bool.
 
 Lemma zerob_false_elim : forall n:nat, zerob n = false -> n <> 0.
-destruct n; [ intro H; inversion H | auto with bool ].
+Proof.
+  destruct n; [ inversion 1 | auto with bool ].
 Qed.
\ No newline at end of file