Now consider remaining conversion problems in solve_remaining_evars.

A step going towards a more uniform evar resolution protocol, currently:
- solve simple constraints (+ actually some heuristics: f.o. unif and
  evar_define's heuristics) but postpone some of the remaining ones [evar_conv]
- try type-classes resolution [resolve_typeclasses]
- apply heuristics on remaining constraints and expect these
  constraints to be resolved [consider_remaining_unif_problems]
- use the implicit tactic for yet open (unconstrained) evars

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

0 files changed, 0 insertions, 0 deletions