diff options
| author | herbelin | 2000-12-18 23:13:00 +0000 |
|---|---|---|
| committer | herbelin | 2000-12-18 23:13:00 +0000 |
| commit | f8f517a6e93fd02595ad96a84dec45377e92640c (patch) | |
| tree | c23a190423780dc01f9d4ba7cf942e953d486eba /theories/Lists | |
| parent | 2660957178fe42aceac95981c580ce7375eea341 (diff) | |
Renommages autour de NewInduction
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1147 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Lists')
| -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 5c0bae6f25..6477d9f0c0 100644 --- a/theories/Lists/PolyList.v +++ b/theories/Lists/PolyList.v @@ -391,7 +391,7 @@ Intros n l d; Generalize n; NewInduction l; Intro n0. Right; Case n0; Trivial. Case n0; Simpl. Auto. -Intro n1; Elim (Hrecl n1); Auto. +Intro n1; Elim (IHl n1); Auto. Save. Lemma nth_S_cons : diff --git a/theories/Lists/TheoryList.v b/theories/Lists/TheoryList.v index 777bbf26cb..f3f87c40e8 100755 --- a/theories/Lists/TheoryList.v +++ b/theories/Lists/TheoryList.v @@ -160,7 +160,7 @@ NewInduction l. Auto. Elim (eqA_dec a a0). Auto. -Simpl. Elim Hrecl; Auto. +Simpl. Elim IHl; Auto. (* Realizer mem. Program_all. |