From 7484a2ab839946f7cb14be190bf92ab3bc5dcafe Mon Sep 17 00:00:00 2001 From: desmettr Date: Thu, 18 Jul 2002 16:48:00 +0000 Subject: 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 --- theories/Reals/Ranalysis4.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'theories/Reals') diff --git a/theories/Reals/Ranalysis4.v b/theories/Reals/Ranalysis4.v index 86e2cececa..111b4bddd1 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 Cut ``0 Cut ``0<=pt``; [Intro | Try Assumption] |[|-(eqT ? (derive_pt ? ? ?) ?)] -> Cut ``0 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 -- cgit v1.2.3