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, 4 insertions, 4 deletions

diff --git a/theories/Lists/PolyList.v b/theories/Lists/PolyList.v
index c1d07eaa6..7eeeb73f0 100644
--- a/theories/Lists/PolyList.v
+++ b/theories/Lists/PolyList.v
@@ -84,9 +84,9 @@ Qed.
 
 Lemma app_eq_nil: (x,y:list) (x^y)=nil -> x=nil /\ y=nil.
 Proof.
- Destruct x;Destruct y;Simpl;Auto.
+ NewDestruct x;NewDestruct y;Simpl;Auto.
  Intros H;Discriminate H.
- Intros a0 l0 H;Discriminate H.
+ Intros;Discriminate H.
 Qed.
 
 Lemma app_cons_not_nil: (x,y:list)(a:A)~nil=(x^(cons a y)).
@@ -101,7 +101,7 @@ Lemma app_eq_unit:(x,y:list)(a:A)
      (x^y)=(cons a nil)-> (x=nil)/\ y=(cons a nil) \/ x=(cons a nil)/\ y=nil.
 
 Proof.
- Destruct x;Destruct y;Simpl.
+ NewDestruct x;NewDestruct y;Simpl.
  Intros a H;Discriminate H.
  Left;Split;Auto.
  Right;Split;Auto.
@@ -442,7 +442,7 @@ i*)
 
 Lemma list_eq_dec : ((x,y:A){x=y}+{~x=y})->(x,y:list){x=y}+{~x=y}.
 Proof.
-  Induction x; Destruct y; Intros; Auto.
+  Induction x; NewDestruct y; Intros; Auto.
   Case (H a a0); Intro e.
   Case (H0 l0); Intro e'.
   Left; Rewrite e; Rewrite e'; Trivial.