diff options
| author | herbelin | 2008-02-13 11:32:04 +0000 |
|---|---|---|
| committer | herbelin | 2008-02-13 11:32:04 +0000 |
| commit | 5b5e0694d6e55b07c38e9d654206aef2b0964ea5 (patch) | |
| tree | 26d059be23064ab343499168773191bf1620a311 /theories | |
| parent | cc12224f791a011a9e495cb3dbd35956abb7ed0d (diff) | |
Essai de prise en compte de delta dans unify_0 (même sur termes non clos).
- Pour éviter de pénaliser auto, eauto, autorewrite, mise en place
d'une option "modulo_conv" pour contrôler l'usage de cette delta.
- Pour éviter que rewrite ne réussise trop souvent, la delta est
désactivée pour les tactiques d'élimination (une étude fine reste à faire).
- On n'utilise aussi delta que sur les sous-termes du problème
d'unification initial. C'est une heuristique qui est intuitive mais qui
reste à être évaluée.
- Au bilan, le surcoût en temps de compilation des theories est d'un
peu moins d'1%.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10557 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories')
| -rw-r--r-- | theories/Reals/Rlimit.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/Reals/Rlimit.v b/theories/Reals/Rlimit.v index 2fb6b22658..f792b84d14 100644 --- a/theories/Reals/Rlimit.v +++ b/theories/Reals/Rlimit.v @@ -560,9 +560,9 @@ Proof. | apply Rlt_le_trans with (Rmin delta1 delta2); [ assumption | apply Rmin_l ] ]. change (0 < eps * (Rsqr l / 2)) in |- *; unfold Rdiv in |- *; - repeat rewrite Rmult_assoc; repeat apply Rmult_lt_0_compat. + repeat rewrite Rmult_assoc; apply Rmult_lt_0_compat. assumption. - apply Rsqr_pos_lt; assumption. + apply Rmult_lt_0_compat. apply Rsqr_pos_lt; assumption. apply Rinv_0_lt_compat; cut (0%nat <> 2%nat); [ intro H3; generalize (lt_INR_0 2 (neq_O_lt 2 H3)); unfold INR in |- *; intro; assumption |