diff options
| author | Matthieu Sozeau | 2014-05-30 14:50:42 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-06-04 15:47:03 +0200 |
| commit | d2a025271724dac2cb129fa0f813a13a686c9972 (patch) | |
| tree | 939b901bd8eeda7c3f61928451cecf58cd1838dc /kernel/inductive.ml | |
| parent | 848f2c41e605287c99e84c2f8ea1747c8a34e201 (diff) | |
- Keep all <= constraints during refinement, otherwise we might miss collapsed universes.
- Fix normalization with universe substitutions during refinement being inconsistent
with the one in the kernel.
Diffstat (limited to 'kernel/inductive.ml')
0 files changed, 0 insertions, 0 deletions