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/Ranalysis3.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/Ranalysis3.v')
| -rw-r--r-- | theories/Reals/Ranalysis3.v | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/theories/Reals/Ranalysis3.v b/theories/Reals/Ranalysis3.v index 9bcde49fd..7728effff 100644 --- a/theories/Reals/Ranalysis3.v +++ b/theories/Reals/Ranalysis3.v @@ -20,9 +20,9 @@ Theorem derivable_pt_lim_div : derivable_pt_lim f2 x l2 -> f2 x <> 0 -> derivable_pt_lim (f1 / f2) x ((l1 * f2 x - l2 * f1 x) / Rsqr (f2 x)). -intros. +intros f1 f2 x l1 l2 H H0 H1. cut (derivable_pt f2 x); - [ intro | unfold derivable_pt in |- *; apply existT with l2; exact H0 ]. + [ intro X | unfold derivable_pt in |- *; apply existT with l2; exact H0 ]. assert (H2 := continuous_neq_0 _ _ (derivable_continuous_pt _ _ X) H1). elim H2; clear H2; intros eps_f2 H2. unfold div_fct in |- *. @@ -756,7 +756,7 @@ Lemma derivable_pt_div : derivable_pt f1 x -> derivable_pt f2 x -> f2 x <> 0 -> derivable_pt (f1 / f2) x. unfold derivable_pt in |- *. -intros. +intros f1 f2 x X X0 H. elim X; intros. elim X0; intros. apply existT with ((x0 * f2 x - x1 * f1 x) / Rsqr (f2 x)). @@ -767,7 +767,7 @@ Lemma derivable_div : forall f1 f2:R -> R, derivable f1 -> derivable f2 -> (forall x:R, f2 x <> 0) -> derivable (f1 / f2). -unfold derivable in |- *; intros. +unfold derivable in |- *; intros f1 f2 X X0 H x. apply (derivable_pt_div _ _ _ (X x) (X0 x) (H x)). Qed. @@ -790,4 +790,4 @@ unfold derive_pt in H; rewrite H in H3. assert (H4 := projT2 pr2). unfold derive_pt in H0; rewrite H0 in H4. apply derivable_pt_lim_div; assumption. -Qed.
\ No newline at end of file +Qed. |