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

1 files changed, 3 insertions, 3 deletions

diff --git a/test-suite/bugs/closed/4390.v b/test-suite/bugs/closed/4390.v
index a96a137001..c069b2d9dc 100644
--- a/test-suite/bugs/closed/4390.v
+++ b/test-suite/bugs/closed/4390.v
@@ -8,16 +8,16 @@ Universe i.
 End foo.
 End M.
 
-Check Type@{i}.
+Check Type@{M.i}.
 (* Succeeds *)
 
 Fail Check Type@{j}.
 (* Error: Undeclared universe: j *)
 
-Definition foo@{j} : Type@{i} := Type@{j}.
+Definition foo@{j} : Type@{M.i} := Type@{j}.
 (* ok *)
 End A.
-
+Import A. Import M.
 Set Universe Polymorphism.
 Fail Universes j.
 Monomorphic Universe j.