diff options
| author | Matthieu Sozeau | 2019-03-15 10:01:16 -0300 |
|---|---|---|
| committer | Matthieu Sozeau | 2019-03-18 20:19:35 +0100 |
| commit | 636857d2e77ee26b4b193f3bbefee253c07dfbff (patch) | |
| tree | f8a5175250d2340aaac6389c7c37ded6c5c93209 /dev | |
| parent | 9ac5483132b42e845a0708491843693b70893eef (diff) | |
[kernel] Fix compare_head_gen_leq_with to use [leq] on applications
This fixes an incompleteness of subtyping on cumulative inductives,
where I@{i} A <= I@{j} A should imply i <= j, i = j or no relation
depending on the variance of I's universe.
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions