Le nouvel Induction s'appelle NewInduction

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

2 files changed, 2 insertions, 2 deletions

diff --git a/theories/Lists/PolyList.v b/theories/Lists/PolyList.v
index 00983c1cf..5c0bae6f2 100644
--- a/theories/Lists/PolyList.v
+++ b/theories/Lists/PolyList.v
@@ -387,7 +387,7 @@ Fixpoint nth_ok [n:nat; l:list] : A->bool :=
 Lemma nth_in_or_default :
   (n:nat)(l:list)(d:A){(In (nth n l d) l)}+{(nth n l d)=d}.
 (** Realizer nth_ok. Program_all. **)
-Intros n l d; Generalize n; Induction l; Intro n0.
+Intros n l d; Generalize n; NewInduction l; Intro n0.
 Right; Case n0; Trivial.
 Case n0; Simpl.
 Auto.
diff --git a/theories/Lists/TheoryList.v b/theories/Lists/TheoryList.v
index bcae01f1a..777bbf26c 100755
--- a/theories/Lists/TheoryList.v
+++ b/theories/Lists/TheoryList.v
@@ -156,7 +156,7 @@ Fixpoint mem [a:A; l:(list A)] : bool :=
 Hints Unfold  In.
 Lemma Mem : (a:A)(l:(list A)){(In a l)}+{(AllS [b:A]~b=a l)}.
 Intros a l.
-Induction l.
+NewInduction l.
 Auto.
 Elim (eqA_dec a a0).
 Auto.