Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states par les fichiers nouvelle syntaxe

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

1 files changed, 18 insertions, 16 deletions

diff --git a/theories/Bool/Zerob.v b/theories/Bool/Zerob.v
index 788025161..6487d08e9 100755
--- a/theories/Bool/Zerob.v
+++ b/theories/Bool/Zerob.v
@@ -8,29 +8,31 @@
 
 (*i $Id$ i*)
 
-Require Arith.
-Require Bool.
+Require Import Arith.
+Require Import Bool.
 
-V7only [Import nat_scope.].
 Open Local Scope nat_scope.
 
-Definition zerob : nat->bool 
-      := [n:nat]Cases n of O => true | (S _) => false end.
+Definition zerob (n:nat) : bool :=
+  match n with
+  | O => true
+  | S _ => false
+  end.
 
-Lemma zerob_true_intro : (n:nat)(n=O)->(zerob n)=true.
-NewDestruct n; [Trivial with bool | Inversion 1].
+Lemma zerob_true_intro : forall n:nat, n = 0 -> zerob n = true.
+destruct n; [ trivial with bool | inversion 1 ].
 Qed.
-Hints Resolve zerob_true_intro : bool.
+Hint Resolve zerob_true_intro: bool.
 
-Lemma zerob_true_elim : (n:nat)(zerob n)=true->(n=O).
-NewDestruct n; [Trivial with bool | Inversion 1].
+Lemma zerob_true_elim : forall n:nat, zerob n = true -> n = 0.
+destruct n; [ trivial with bool | inversion 1 ].
 Qed.
 
-Lemma zerob_false_intro : (n:nat)~(n=O)->(zerob n)=false.
-NewDestruct n; [NewDestruct 1; Auto with bool | Trivial with bool].
+Lemma zerob_false_intro : forall n:nat, n <> 0 -> zerob n = false.
+destruct n; [ destruct 1; auto with bool | trivial with bool ].
 Qed.
-Hints Resolve zerob_false_intro : bool.
+Hint Resolve zerob_false_intro: bool.
 
-Lemma zerob_false_elim : (n:nat)(zerob n)=false -> ~(n=O).
-NewDestruct n; [Intro H; Inversion H | Auto with bool].
-Qed.
+Lemma zerob_false_elim : forall n:nat, zerob n = false -> n <> 0.
+destruct n; [ intro H; inversion H | auto with bool ].
+Qed.
\ No newline at end of file