diff options
| author | Hugo Herbelin | 2020-09-16 15:05:12 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-09-28 11:42:43 +0200 |
| commit | 772aa6bd5659d466b92ea33c997012414b0f946c (patch) | |
| tree | cb5f9b0e1bc66ac6cde25cb635c1bd965c887325 /dev | |
| parent | 9c2228ff011dc6188b70084fa1e1a5158affcf24 (diff) | |
More precise information when unification fails because of incompatible candidates.
We also show the incompatible contender.
Ideally, we should also remember the source of the other contender.
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions