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

diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index f6052b368..a1323e501 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -15,6 +15,7 @@ open Term
 open Sign
 open Libnames
 open Mod_subst
+open Termops
 (*i*)
 
 (* The type of mappings for existential variables.
@@ -174,6 +175,8 @@ val meta_reassign  : metavariable -> constr * instance_status -> evar_defs -> ev
 (* [meta_merge evd1 evd2] returns [evd2] extended with the metas of [evd1] *)
 val meta_merge : evar_defs -> evar_defs -> evar_defs
 
+val metas_of : evar_defs -> metamap
+
 (**********************************************************)
 (* Sort variables *)