From 735070100540076e715792bf17fa291e4a4cbfd5 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 26 Nov 2000 19:05:54 +0000
Subject: Le nouvel Induction s'appelle NewInduction

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@965 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Lists/PolyList.v   | 2 +-
 theories/Lists/TheoryList.v | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/theories/Lists/PolyList.v b/theories/Lists/PolyList.v
index 00983c1cfa..5c0bae6f25 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 bcae01f1a7..777bbf26cb 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.
-- 
cgit v1.2.3