*** empty log message ***

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

1 files changed, 7 insertions, 10 deletions

diff --git a/theories/Lists/PolyList.v b/theories/Lists/PolyList.v
index 817d06ce2..cd56ba1de 100644
--- a/theories/Lists/PolyList.v
+++ b/theories/Lists/PolyList.v
@@ -437,22 +437,19 @@ Definition nth_default : A -> list -> nat -> A :=
 Lemma nth_In :
   (n:nat)(l:list)(d:A)(lt n (length l))->(In (nth n l d) l).
 
-Proof. 
-  Intros n l d.
-  Generalize n; Clear n.
-  NewInduction l.
-    Inversion 1.
-  Simpl.
-  NewInduction n.
-    Auto.
-  Right;Auto with arith.
+Proof.
+Unfold lt; Induction n ; Simpl.
+Induction l ; Simpl ;  [ Inversion 2 | Auto].
+Clear n ; Intros n hn ; Induction l ; Simpl.
+Inversion 2.
+Clear l ; Intros a l hl d ie ; Right ; Apply hn ; Auto with arith.
 Qed.
 
-
 (********************************)
 (** Decidable equality on lists *)
 (********************************)
 
+
 Lemma list_eq_dec : ((x,y:A){x=y}+{~x=y})->(x,y:list){x=y}+{~x=y}.
 Proof.
   Induction x; NewDestruct y; Intros; Auto.