From 5b5e0694d6e55b07c38e9d654206aef2b0964ea5 Mon Sep 17 00:00:00 2001 From: herbelin Date: Wed, 13 Feb 2008 11:32:04 +0000 Subject: 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%. MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10557 85f007b7-540e-0410-9357-904b9bb8a0f7 --- proofs/clenvtac.mli | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'proofs/clenvtac.mli') 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 *) -- cgit v1.2.3