diff options
| author | Gaëtan Gilbert | 2021-01-11 12:12:45 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2021-01-11 12:13:00 +0100 |
| commit | 925794c34d08752cee85362d1c2772559e89d2c9 (patch) | |
| tree | ea1821bb86fc0d62b2ac09b9fe0650fc9d97070a /kernel/nativecode.mli | |
| parent | 27a9a28e8628c94910a08efc2f611e91e3e553bb (diff) | |
Fix #13732: Implicit Type vs universes
This returns to the previous behaviour of Implicit Type forgetting
universes.
`Implicit Type T : Type@{u}.` may be confusing as it is equivalent to
`: Type`, but until we have a better idea of what to do with anonymous
types I see no other solution, especially in the short term to fix the
bug.
Diffstat (limited to 'kernel/nativecode.mli')
0 files changed, 0 insertions, 0 deletions