diff options
| author | Hugo Herbelin | 2020-10-29 16:49:25 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2020-10-31 20:29:48 +0100 |
| commit | f8f915df4a8e3c619a4ccb204ea16afacf983430 (patch) | |
| tree | 927f5b2f370dda64c6be5f4c651fdbebd57b200f /kernel/type_errors.mli | |
| parent | 710f74901e0fd65ca677555366cae3d00686c9c8 (diff) | |
Closes #13278: take into account elimination constraints in small inversion.
Ideally, if equations t <= ?x were preserving subtyping that could be
simpler. Currently we need however to put a rigid universe as
constraint on the return predicate so that one branch does not force
the return sort to be lower by unification than what another branch
would have needed.
Diffstat (limited to 'kernel/type_errors.mli')
0 files changed, 0 insertions, 0 deletions