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 /pretyping/pretype_errors.mli | |
| 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 'pretyping/pretype_errors.mli')
| -rw-r--r-- | pretyping/pretype_errors.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli index 70f218d617..45997e9a66 100644 --- a/pretyping/pretype_errors.mli +++ b/pretyping/pretype_errors.mli @@ -23,6 +23,7 @@ type unification_error = | NotSameHead | NoCanonicalStructure | ConversionFailed of env * constr * constr + | IncompatibleInstances of env * existential * constr * constr | MetaOccurInBody of Evar.t | InstanceNotSameType of Evar.t * env * types * types | UnifUnivInconsistency of Univ.univ_inconsistency |