Essai d'une nouvelle heuristique pour clenv_unique_resolver : si le

lemme n'est pas un lemme d'induction (plus précisément si la tête de
la conclusion n'est pas une variable), alors on n'instancie pas les
with-bindings pour que les unifications venant du filtrage de la
conclusion du lemme avec le but soient prioritaires (en effet
l'utilisation des types des with-bindings pour inférer des instances
-- portion du commit r9842 -- ne produit pas des solutions exactes
mais seulement des sous-types de solutions exactes alors que
l'unification avec le but produit des solutions exactes qui doivent
donc être considérées en priorité). Toutefois, dans certains cas, du
fait que unify_0 travaille modulo conversion uniquement sur les termes
clos, il faut quand même donner crédit aux instances données en
with-bindings pour que la conversion puisse être prise en compte et
ainsi retrouver un comportement au moins identique au précédent.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9847 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 6 insertions, 9 deletions

diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml
index 929535b76..c563688a8 100644
--- a/pretyping/clenv.ml
+++ b/pretyping/clenv.ml
@@ -67,13 +67,7 @@ let clenv_type clenv = meta_instance clenv.evd clenv.templtyp
 let clenv_hnf_constr ce t = hnf_constr (cl_env ce) (cl_sigma ce) t
 
 let clenv_get_type_of ce c =
-  let metamap =
-    List.map 
-      (function
-	 | (n,Clval(_,_,typ)) -> (n,typ.rebus)
-         | (n,Cltyp (_,typ))    -> (n,typ.rebus))
-      (meta_list ce.evd) in
-  Retyping.get_type_of_with_meta (cl_env ce) (cl_sigma ce) metamap c
+  Retyping.get_type_of_with_meta (cl_env ce) (cl_sigma ce) (metas_of ce.evd) c
 
 exception NotExtensibleClause
 
@@ -255,8 +249,11 @@ let clenv_unify allow_K cv_pb t1 t2 clenv =
   { clenv with evd = w_unify allow_K clenv.env cv_pb t1 t2 clenv.evd }
 
 let clenv_unique_resolver allow_K clenv gl =
-  clenv_unify allow_K CUMUL (clenv_type clenv) (pf_concl gl) clenv
-
+  if isMeta (fst (whd_stack clenv.templtyp.rebus)) then
+    clenv_unify allow_K CUMUL (clenv_type clenv) (pf_concl gl) clenv
+  else
+    try clenv_unify allow_K CUMUL clenv.templtyp.rebus (pf_concl gl) clenv
+    with _ -> clenv_unify allow_K CUMUL (clenv_type clenv) (pf_concl gl) clenv
 
 (* [clenv_pose_dependent_evars clenv]
  * For each dependent evar in the clause-env which does not have a value,