Introducing a notion of evar candidates to be used when an evar is

known in advance to be instantiable by only a finite number of terms.
When an evar with candidates remain unsolved after unification, the
first candidate is taken as a heuristic.

This is used in particular to reduce the number of pending conversion
problems when trying to infer the return clause of a pattern-matching
problem. As an example, this repairs test 2615.v.

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

0 files changed, 0 insertions, 0 deletions