diff options
| author | Gaëtan Gilbert | 2018-10-18 13:59:38 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-11-12 18:43:04 +0100 |
| commit | 7a3b6b644f85489dced02b33712ad21afe0df47d (patch) | |
| tree | 37cc8f21ec113ae70c2ac0c0c0cc09555ddeaa7e /engine | |
| parent | 81e7467a3db24887e1d4026ee8441846eb09309a (diff) | |
Don't declare universe binders for variables.
Otherwise
~~~
Unset Strict Universe Declaration.
Section bar.
Let baz := Type@{u}.
Definition k := baz.
End bar.
Section bar.
Let baz := Type@{u}.
Definition k' := baz.
End bar.
~~~
is broken (and has been since we stopped checking for repeated section names).
Diffstat (limited to 'engine')
0 files changed, 0 insertions, 0 deletions