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

3 files changed, 26 insertions, 5 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index ebba4b00bb..92786e0896 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -561,7 +561,11 @@ let priority l = List.map snd (List.filter (fun (pr,_) -> pr = 0) l)
 
 open Unification
 
-let auto_unif_flags = { modulo_delta = true; use_metas_eagerly = false }
+let auto_unif_flags = {
+  modulo_conv_on_closed_terms = true; 
+  use_metas_eagerly = false;
+  modulo_conv = false; 
+}
 
 (* Try unification with the precompiled clause, then use registered Apply *)
 
diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml
index fb25d9d25d..0214a940cb 100644
--- a/tactics/setoid_replace.ml
+++ b/tactics/setoid_replace.ml
@@ -1731,8 +1731,17 @@ let check_evar_map_of_evars_defs evd =
 (* [unification_rewrite] searchs a match for [c1] in [but] and then 
    returns the modified objects (in particular [c1] and [c2]) *)  
 
-let rewrite_unif_flags = { modulo_delta = false; use_metas_eagerly = true }
-let rewrite2_unif_flags = { modulo_delta = true; use_metas_eagerly = true }
+let rewrite_unif_flags = {
+  modulo_conv_on_closed_terms = false;
+  use_metas_eagerly = true;
+  modulo_conv = false
+}
+
+let rewrite2_unif_flags = {
+  modulo_conv_on_closed_terms = true;
+  use_metas_eagerly = true;
+  modulo_conv = false
+ }
 
 let unification_rewrite c1 c2 cl but gl = 
   let (env',c1) =
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 39765526f0..fa40e16514 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -43,6 +43,7 @@ open Decl_kinds
 open Evarutil
 open Indrec
 open Pretype_errors
+open Unification
 
 exception Bound
 
@@ -822,7 +823,13 @@ let last_arg c = match kind_of_term c with
   | App (f,cl) ->  
       array_last cl
   | _ -> anomaly "last_arg"
-	
+
+let elim_flags = {
+  modulo_conv_on_closed_terms = true; 
+  use_metas_eagerly = true;
+  modulo_conv = false
+}
+
 let elimination_clause_scheme with_evars allow_K elimclause indclause gl = 
   let indmv = 
     (match kind_of_term (last_arg elimclause.templval.rebus) with
@@ -831,7 +838,8 @@ let elimination_clause_scheme with_evars allow_K elimclause indclause gl =
              (str "The type of elimination clause is not well-formed")) 
   in
   let elimclause' = clenv_fchain indmv elimclause indclause in 
-  res_pf elimclause' ~with_evars:with_evars ~allow_K:allow_K gl
+  res_pf elimclause' ~with_evars:with_evars ~allow_K:allow_K ~flags:elim_flags
+    gl
 
 (* cast added otherwise tactics Case (n1,n2) generates (?f x y) and 
  * refine fails *)