Expérimentation de NewDestruct et parfois NewInduction

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

1 files changed, 5 insertions, 5 deletions

diff --git a/theories/Arith/Peano_dec.v b/theories/Arith/Peano_dec.v
index b02d5a324..d847a060d 100755
--- a/theories/Arith/Peano_dec.v
+++ b/theories/Arith/Peano_dec.v
@@ -12,20 +12,20 @@ Require Decidable.
 
 Theorem O_or_S : (n:nat)({m:nat|(S m)=n})+{O=n}.
 Proof.
-Induction n.
+NewInduction n.
 Auto.
-Intros p H; Left; Exists p; Auto.
+Left; Exists n; Auto.
 Qed.
 
 Theorem eq_nat_dec : (n,m:nat){n=m}+{~(n=m)}.
 Proof.
-Induction n; Induction m; Auto.
-Intros q H'; Elim (H q); Auto.
+NewInduction n; NewInduction m; Auto.
+Elim (IHn m); Auto.
 Qed.
 
 Hints Resolve O_or_S eq_nat_dec : arith.
 
 Theorem dec_eq_nat:(x,y:nat)(decidable (x=y)).
 Intros x y; Unfold decidable; Elim (eq_nat_dec x y); Auto with arith.
-Save.
+Qed.