diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2017-12-01 10:11:41 +0100 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2017-12-01 10:16:49 +0100 |
| commit | 20c98eab851210702b39e1c66e005acfc351d8dd (patch) | |
| tree | 957aab7aadfda8c10f251ff9d83f3f5b05c07dc5 /vernac/classes.ml | |
| parent | 0048cbe810c82a775558c14cd7fcae644e205c51 (diff) | |
Proper nametab handling of global universe names
They are now bound at the library + module level and can be qualified
and shadowed according to the usual rules of qualified names.
Parsing and printing of universes "u+n" done as well.
In sections, global universes are discharged as well, checking that
they can be defined globally when they are introduced
Diffstat (limited to 'vernac/classes.ml')
0 files changed, 0 insertions, 0 deletions