diff options
| author | Hugo Herbelin | 2020-10-29 16:50:09 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2020-10-31 19:48:56 +0100 |
| commit | 710f74901e0fd65ca677555366cae3d00686c9c8 (patch) | |
| tree | fec946ee025043ef13c263d6445efd0eaeb24234 /kernel/type_errors.mli | |
| parent | 391898b6bd83a80ec7f7bd4ac2b9d20874f76773 (diff) | |
Fine-tuning the sort of the predicate obtained by small inversion.
If the result is in SProp, Prop or (impredicative) Set, we preserve
this information since the elimination sort might be restricted by the
sort of the destructed type.
If the result is in Type, we use a fresh sort upper bound so that we
are sure not having residual algebraic universes which would raise
problems in a type constraint (e.g. in define_evar_as_product).
This fixes the part of #13278 posted on discourse.
Diffstat (limited to 'kernel/type_errors.mli')
0 files changed, 0 insertions, 0 deletions