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, 0 deletions

diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 5d959be8bd..1ff0c633a0 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -464,6 +464,12 @@ let pr_sort_constraints (_,sm) = pr_sort_cstrs sm
 
 let meta_list evd = metamap_to_list evd.metas
 
+let metas_of evd = 
+  List.map (function
+    | (n,Clval(_,_,typ)) -> (n,typ.rebus)
+    | (n,Cltyp (_,typ))  -> (n,typ.rebus))
+    (meta_list evd)
+
 let meta_defined evd mv =
   match Metamap.find mv evd.metas with
     | Clval _ -> true