Tentatively starting to use heuristics for evar-evar resolution: first

step, prefer QuestionMark's to other evars, to comply with the
filtering made on VarInstance, GoalEvar and QuestionMark for type
class resolution. Maybe evars to be resolved by type class instances
should eventually be marked with a specific tag.

At least, this solves the current problem with compiling cancel2.v in
LemmaOverloading.

0 files changed, 0 insertions, 0 deletions