Generalized the use of evar candidates in type inference unification:

- use evar candidates instead of postponed conversion problems when
  it is known (according to the projection heuristic used) that an
  evar has only a fixed number of possible instances (as e.g. in
  equation ?n[x,x] = x, with x a variable);
- this allows to be more robust in solving remaining problems: if
  several instanciations exist, and one is not compatible with a previous
  instantiation made among several choices for another evar,
  backtracking is now possible;
- this allows in particular to fix regression #2670 (two postponed
  conversion problems solved in an inconsistent way);
- but this requires more code.

At the same time, a refactoring of the code has been made so as to
hopefully clarify the elementary pieces of the algorithm. For
instance, there are now generic functions for both applying a filter
and giving candidates. The filter is systematically generalized so as
to have the ccl of the evar well-typed even in situations where we
could try on the contrary to restrict the evars occurring in the
ccl.

Anyway, when the representation of instances will be optimized using
identity substitutions, it will no longer be useful to use the filter
to shorten the size of the instances. Then, the filters will have,
like candidates, the only role of restricting the search space for
potential solutions to the unification problems.

Also, solve_refl can now be used to restrict equations ?x[t1..tn]=?x[u1..un]
up to conversion instead of up to unification. This (potententially)
looses constraints but this avoids looping at the time of considering
remaining problems and applying heuristics to them.

Also added printing of evar candidates in debugging evar printers

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

0 files changed, 0 insertions, 0 deletions