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/Rtrigo_reg.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/Rtrigo_reg.v')
| -rw-r--r-- | theories/Reals/Rtrigo_reg.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/theories/Reals/Rtrigo_reg.v b/theories/Reals/Rtrigo_reg.v index 0fb8ee387..d9e96b9c5 100644 --- a/theories/Reals/Rtrigo_reg.v +++ b/theories/Reals/Rtrigo_reg.v @@ -32,7 +32,7 @@ cut (fun n:nat => sum_f_R0 (fun k:nat => Rabs (/ INR (fact (2 * k)) * r ^ (2 * k))) n) l)). -intro; elim X; intros. +intro X; elim X; intros. apply existT with x. split. apply p. @@ -206,7 +206,7 @@ cut sum_f_R0 (fun k:nat => Rabs (/ INR (fact (2 * k + 1)) * r ^ (2 * k))) n) l)). -intro; elim X; intros. +intro X; elim X; intros. apply existT with x. split. apply p. @@ -605,4 +605,4 @@ Lemma derive_pt_cos : forall x:R, derive_pt cos x (derivable_pt_cos _) = - sin x. intros; apply derive_pt_eq_0. apply derivable_pt_lim_cos. -Qed.
\ No newline at end of file +Qed. |