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/Ranalysis4.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/Ranalysis4.v')
| -rw-r--r-- | theories/Reals/Ranalysis4.v | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/theories/Reals/Ranalysis4.v b/theories/Reals/Ranalysis4.v index 16f79fd1e..0aeb5e1b7 100644 --- a/theories/Reals/Ranalysis4.v +++ b/theories/Reals/Ranalysis4.v @@ -20,13 +20,13 @@ Require Import Exp_prop. Open Local Scope R_scope. Lemma derivable_pt_inv : forall (f:R -> R) (x:R), f x <> 0 -> derivable_pt f x -> derivable_pt (/ f) x. -intros; cut (derivable_pt (fct_cte 1 / f) x -> derivable_pt (/ f) x). -intro; apply X0. +intros f x H X; cut (derivable_pt (fct_cte 1 / f) x -> derivable_pt (/ f) x). +intro X0; apply X0. apply derivable_pt_div. apply derivable_pt_const. assumption. assumption. -unfold div_fct, inv_fct, fct_cte in |- *; intro; elim X0; intros; +unfold div_fct, inv_fct, fct_cte in |- *; intro X0; elim X0; intros; unfold derivable_pt in |- *; apply existT with x0; unfold derivable_pt_abs in |- *; unfold derivable_pt_lim in |- *; unfold derivable_pt_abs in p; unfold derivable_pt_lim in p; @@ -76,8 +76,8 @@ Qed. (**********) Lemma derivable_inv : forall f:R -> R, (forall x:R, f x <> 0) -> derivable f -> derivable (/ f). -intros. -unfold derivable in |- *; intro. +intros f H X. +unfold derivable in |- *; intro x. apply derivable_pt_inv. apply (H x). apply (X x). @@ -381,4 +381,4 @@ Lemma derive_pt_sinh : forall x:R, derive_pt sinh x (derivable_pt_sinh x) = cosh x. intro; apply derive_pt_eq_0. apply derivable_pt_lim_sinh. -Qed.
\ No newline at end of file +Qed. |