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

1 files changed, 15 insertions, 5 deletions

diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index ad19bd9b6..ced684965 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -67,15 +67,17 @@ let clenv_refine with_evars clenv gls =
     (refine (clenv_cast_meta clenv (clenv_value clenv)))
     gls
 
+let dft = Unification.default_unify_flags
 
-let res_pf clenv ?(with_evars=false) ?(allow_K=false) gls =
-  clenv_refine with_evars (clenv_unique_resolver allow_K clenv gls) gls
+let res_pf clenv ?(with_evars=false) ?(allow_K=false) ?(flags=dft) gls =
+  clenv_refine with_evars
+    (clenv_unique_resolver allow_K ~flags:flags clenv gls) gls
 
-let elim_res_pf_THEN_i clenv tac gls =  
+let elim_res_pf_THEN_i clenv tac gls =
   let clenv' = (clenv_unique_resolver true clenv gls) in
   tclTHENLASTn (clenv_refine false clenv') (tac clenv') gls
 
-let e_res_pf clenv = res_pf clenv ~with_evars:true ~allow_K:false
+let e_res_pf clenv = res_pf clenv ~with_evars:true ~allow_K:false ~flags:dft
 
 
 (* [unifyTerms] et [unify] ne semble pas gérer les Meta, en
@@ -83,11 +85,19 @@ let e_res_pf clenv = res_pf clenv ~with_evars:true ~allow_K:false
    d'une même Meta sont compatibles. D'ailleurs le "fst" jette les metas
    provenant de w_Unify. (Utilisé seulement dans prolog.ml) *)
 
+open Unification
+
+let fail_quick_unif_flags = {
+  modulo_conv_on_closed_terms = true; 
+  use_metas_eagerly = false;
+  modulo_conv = false; 
+}
+
 (* let unifyTerms m n = walking (fun wc -> fst (w_Unify CONV m n [] wc)) *)
 let unifyTerms m n gls = 
   let env = pf_env gls in
   let evd = create_goal_evar_defs (project gls) in
-  let evd' = Unification.w_unify false env CONV m n evd in
+  let evd' = w_unify false env CONV ~flags:fail_quick_unif_flags m n evd in
   tclIDTAC {it = gls.it; sigma = evars_of evd'}
 
 let unify m gls =