diff options
| author |  desmettr <desmettr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-07-18 16:48:00 +0000 |
|---|---|---|
| committer | desmettr <desmettr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-07-18 16:48:00 +0000 |
| commit | 7484a2ab839946f7cb14be190bf92ab3bc5dcafe (patch) | |
| tree | 35329c3c20d0dd9a2036772074e91830325d2dd6 /theories/Reals/Ranalysis4.v | |
| parent | 78ab4244f2059844e9ebb1b1ba6d24ab764015e9 (diff) | |
Correction d'un bug dans IsCont_pt
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2899 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Reals/Ranalysis4.v')
| -rw-r--r-- | theories/Reals/Ranalysis4.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/Reals/Ranalysis4.v b/theories/Reals/Ranalysis4.v index 86e2cecec..111b4bddd 100644 --- a/theories/Reals/Ranalysis4.v +++ b/theories/Reals/Ranalysis4.v @@ -292,7 +292,7 @@ Match trm With |[sqrt] -> (Match Context With |[|-(derivable_pt ? ?)] -> Cut ``0<pt``; [Intro | Try Assumption] - |[|-(continuity_pt ? ?)] -> Cut ``0<pt``; [Intro | Try Assumption] + |[|-(continuity_pt ? ?)] -> Cut ``0<=pt``; [Intro | Try Assumption] |[|-(eqT ? (derive_pt ? ? ?) ?)] -> Cut ``0<pt``; [Intro | Try Assumption] | _ -> Idtac) |[?1] -> Let p = ?1 In @@ -420,7 +420,7 @@ Match Context With |[|-(continuity_pt sinh ?)] -> Apply derivable_continuous_pt; Apply derivable_pt_sinh |[|-(continuity_pt cosh ?)] -> Apply derivable_continuous_pt; Apply derivable_pt_cosh |[|-(continuity_pt exp ?)] -> Apply derivable_continuous_pt; Apply derivable_pt_exp -|[|-(derivable_pt sqrt ?1)] -> Apply derivable_continuous_pt; Apply (derivable_pt_sqrt ?1); Assumption Orelse Unfold plus_fct minus_fct opp_fct mult_fct div_fct inv_fct comp id fct_cte +|[|-(continuity_pt sqrt ?1)] -> Apply continuity_pt_sqrt; Assumption Orelse Unfold plus_fct minus_fct opp_fct mult_fct div_fct inv_fct comp id fct_cte (* regles de differentiabilite *) (* PLUS *) |[|-(continuity_pt (plus_fct ?1 ?2) ?3)] -> Apply (continuity_pt_plus ?1 ?2 ?3); IsCont_pt |