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 /doc/common/styles/html/coqremote/modules/node/node.css | |
| 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 'doc/common/styles/html/coqremote/modules/node/node.css')
0 files changed, 0 insertions, 0 deletions