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.ml | |
| 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.ml')
| -rw-r--r-- | pretyping/pretype_errors.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml index 207ffc7b86..1e8441dd8a 100644 --- a/pretyping/pretype_errors.ml +++ b/pretyping/pretype_errors.ml @@ -20,6 +20,7 @@ type unification_error = | NotSameHead | NoCanonicalStructure | ConversionFailed of env * constr * constr (* Non convertible closed terms *) + | IncompatibleInstances of env * existential * constr * constr | MetaOccurInBody of Evar.t | InstanceNotSameType of Evar.t * env * types * types | UnifUnivInconsistency of Univ.univ_inconsistency |