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

3 files changed, 3 insertions, 3 deletions

diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v
index 2c5c0f569d..8c3ade1cd8 100755
--- a/theories/Init/Logic.v
+++ b/theories/Init/Logic.v
@@ -150,7 +150,7 @@ Section Logic_lemmas.
   Proof.
    Intros.
    Cut (identity A x y).
-   Destruct 1; Auto.
+   NewDestruct 1; Auto.
    Elim H; Auto.
   Qed.
 
diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v
index eb7edad110..4882ea29ca 100755
--- a/theories/Init/Specif.v
+++ b/theories/Init/Specif.v
@@ -189,7 +189,7 @@ Lemma False_rect: (C:Type)False->C.
 Proof.
   Intros.
   Cut Empty_set.
-  Destruct 1.
+  NewDestruct 1.
   Elim H.
 Qed.
 
diff --git a/theories/Init/Wf.v b/theories/Init/Wf.v
index 214c33117d..bd55dcd1d8 100755
--- a/theories/Init/Wf.v
+++ b/theories/Init/Wf.v
@@ -29,7 +29,7 @@ Chapter Well_founded.
     := Acc_intro : (x:A)((y:A)(R y x)->(Acc y))->(Acc x).
 
  Lemma Acc_inv : (x:A)(Acc x) -> (y:A)(R y x) -> (Acc y).
-  Destruct 1; Trivial.
+  NewDestruct 1; Trivial.
  Defined.
 
   (* the informative elimination :