diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-03-28 22:16:14 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-03-28 22:16:14 +0000 |
| commit | b730066fb4dfdeccd7b17538eda845d0048c68ca (patch) | |
| tree | 25e10bc3b9780ded7cbc6e7c27dc0c0993f966f0 /theories/Reals/SeqSeries.v | |
| parent | 98af1982684a02f9521d28594e0fa01ac3275083 (diff) | |
Nommage explicite de certains "intro" pour préserver la compatibilité
en préparation du passage à des inductifs à polymorphisme de sorte
("sigT R" va devenir de type le type de R, càd Set)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8670 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Reals/SeqSeries.v')
| -rw-r--r-- | theories/Reals/SeqSeries.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/theories/Reals/SeqSeries.v b/theories/Reals/SeqSeries.v index 7a02b689d..f3762bd7b 100644 --- a/theories/Reals/SeqSeries.v +++ b/theories/Reals/SeqSeries.v @@ -36,12 +36,12 @@ intros; (sigT (fun l:R => Un_cv (fun n:nat => sum_f_R0 (fun l:nat => fn (S N + l)%nat x) n) l)). -intro; +intro X; cut (sigT (fun l:R => Un_cv (fun n:nat => sum_f_R0 (fun l:nat => An (S N + l)%nat) n) l)). -intro; elim X; intros l1N H2. +intro X0; elim X; intros l1N H2. elim X0; intros l2N H3. cut (l1 - SP fn N x = l1N). intro; cut (l2 - sum_f_R0 An N = l2N). @@ -217,7 +217,7 @@ Lemma Rseries_CV_comp : (forall n:nat, 0 <= An n <= Bn n) -> sigT (fun l:R => Un_cv (fun N:nat => sum_f_R0 Bn N) l) -> sigT (fun l:R => Un_cv (fun N:nat => sum_f_R0 An N) l). -intros; apply cv_cauchy_2. +intros An Bn H X; apply cv_cauchy_2. assert (H0 := cv_cauchy_1 _ X). unfold Cauchy_crit_series in |- *; unfold Cauchy_crit in |- *. intros; elim (H0 eps H1); intros. |