diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-02-13 11:32:04 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-02-13 11:32:04 +0000 |
| commit | 5b5e0694d6e55b07c38e9d654206aef2b0964ea5 (patch) | |
| tree | 26d059be23064ab343499168773191bf1620a311 /proofs/clenvtac.mli | |
| 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 'proofs/clenvtac.mli')
| -rw-r--r-- | proofs/clenvtac.mli | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/proofs/clenvtac.mli b/proofs/clenvtac.mli index 038f84f01..90d010c80 100644 --- a/proofs/clenvtac.mli +++ b/proofs/clenvtac.mli @@ -17,12 +17,13 @@ open Evd open Clenv open Proof_type open Tacexpr +open Unification (*i*) (* Tactics *) val unify : constr -> tactic val clenv_refine : evars_flag -> clausenv -> tactic -val res_pf : clausenv -> ?with_evars:evars_flag -> ?allow_K:bool -> tactic +val res_pf : clausenv -> ?with_evars:evars_flag -> ?allow_K:bool -> ?flags:unify_flags -> tactic val elim_res_pf_THEN_i : clausenv -> (clausenv -> tactic array) -> tactic (* Compatibility, use res_pf ?with_evars:true instead *) |