diff options
| -rw-r--r-- | theories/Lists/PolyList.v | 2 | ||||
| -rwxr-xr-x | 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. |