Abandon unification pattern des evars dans apply: combiné avec le

backtrack de eauto et le partage des evars entre buts, cela fait
davantage de choix irréversibles avec rupture de compatibilité.
Exemple: 
   but 1: |- P ?f
   but 2: H1:a=b, H2:c=c, H3:g a = g b |- ?f a = ?f b
   eauto sur le but 2 peut trouver au moins 3 solutions:
     1- avec unif premier ordre, il peut trouver ?f=g, en appliquant exact H3
     2- avec unif pattern, il peut trouver ?f=\_.c, en appliquant exact H2
     3- en s'y prenant bien, il devrait pouvoir laisser ?f ouvert en appliquant
        f_equal H1
Dans certains exemples (Orsay/FSets/PrecedenceGraph/PrecedenceGraph.v en
l'occurrence), ajouter l'unif pattern fait adopter la solution 2
plutôt que la solution 3. En attente d'un meilleur algorithme, abandon
donc de l'unif pattern des evars pour apply (ce qui n'empêche pas que,
déjà, la situation actuelle, qui utilise l'unif premier ordre, peut
conduire à faire des mauvais choix -- mais au moins on reste
compatible...).


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

0 files changed, 0 insertions, 0 deletions