diff options
| author | Hugo Herbelin | 2018-04-26 15:51:03 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2018-09-27 14:21:10 +0200 |
| commit | 8ef1be1aead0dbcc2d3cc46a7e5eaa02f9ad6069 (patch) | |
| tree | 60e562a2662a8a499c359c2454a37425d217b1c7 /tools | |
| parent | cfefed1cb20b6abe33c222df49d346867bafbc7f (diff) | |
Unification failure: don't give preference to a "beyond capabilities" error.
This is actually a bit ad hoc at this stage in the sense that this is
specifically to prefer an informative first-order unification failure
over the currently always uninformative failure coming from
second-order unification.
When second-order unification shall be able to give more information,
one may consider alternative strategies, even maybe reporting not just
one but the list of failures in all (interesting) branches.
Diffstat (limited to 'tools')
0 files changed, 0 insertions, 0 deletions