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, 13 insertions, 6 deletions

diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index bce5710d6..2abbc389f 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -150,10 +150,15 @@ let tag_var = tag Tag.variable
 
   let pr_sep_com sep f c = pr_with_comments ?loc:(constr_loc c) (sep() ++ f c)
 
+  let pr_univ_expr = function
+    | Some (x,n) ->
+       pr_reference x ++ (match n with 0 -> mt () | _ -> str"+" ++ int n)
+    | None -> str"_"
+
   let pr_univ l =
     match l with
-      | [_,x] -> Name.print x
-      | l -> str"max(" ++ prlist_with_sep (fun () -> str",") (fun x -> Name.print (snd x)) l ++ str")"
+      | [x] -> pr_univ_expr x
+      | l -> str"max(" ++ prlist_with_sep (fun () -> str",") pr_univ_expr l ++ str")"
 
   let pr_univ_annot pr x = str "@{" ++ pr x ++ str "}"
 
@@ -166,8 +171,9 @@ let tag_var = tag Tag.variable
   let pr_glob_level = function
     | GProp -> tag_type (str "Prop")
     | GSet -> tag_type (str "Set")
-    | GType None -> tag_type (str "Type")
-    | GType (Some (_, u)) -> tag_type (Name.print u)
+    | GType UUnknown -> tag_type (str "Type")
+    | GType UAnonymous -> tag_type (str "_")
+    | GType (UNamed u) -> tag_type (pr_reference u)
 
   let pr_qualid sp =
     let (sl, id) = repr_qualid sp in
@@ -192,8 +198,9 @@ let tag_var = tag Tag.variable
       tag_type (str "Set")
     | GType u ->
       (match u with
-        | Some (_,u) -> Name.print u
-        | None -> tag_type (str "Type"))
+        | UNamed u -> pr_reference u
+        | UAnonymous -> tag_type (str "Type")
+        | UUnknown -> tag_type (str "_"))
 
   let pr_universe_instance l =
     pr_opt_no_spc (pr_univ_annot (prlist_with_sep spc pr_glob_sort_instance)) l