diff options
| author | Hugo Herbelin | 2014-12-15 19:14:51 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2014-12-15 19:18:42 +0100 |
| commit | 0cf1f6447870998d0b58667d4dbe1c65faa3b723 (patch) | |
| tree | 77c8c55bdbd370f075380947f4228efd55ca151b /plugins/syntax/string_syntax_plugin.mllib | |
| parent | c73f114a46d50ab7c22218db0e80d5da96a824e4 (diff) | |
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.
Diffstat (limited to 'plugins/syntax/string_syntax_plugin.mllib')
0 files changed, 0 insertions, 0 deletions