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

3 files changed, 65 insertions, 46 deletions

diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 0d1e401d9..6527ba935 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -414,15 +414,17 @@ let detype_case computable detype detype_eqns testdep avoid data p c bl =
       let eqnl = detype_eqns constructs constagsl bl in
       GCases (tag,pred,[tomatch,(alias,aliastyp)],eqnl)
 
+let detype_universe sigma u =
+  let fn (l, n) = Some (Termops.reference_of_level sigma l, n) in
+  Univ.Universe.map fn u
+
 let detype_sort sigma = function
   | Prop Null -> GProp
   | Prop Pos -> GSet
   | Type u ->
     GType
       (if !print_universes
-       then
-         let u = Pp.string_of_ppcmds (Univ.Universe.pr_with (Termops.pr_evd_level sigma) u) in
-         [Loc.tag @@ Name.mk_name (Id.of_string_soft u)]
+       then detype_universe sigma u
        else [])
 
 type binder_kind = BProd | BLambda | BLetIn
@@ -434,8 +436,8 @@ let detype_anonymous = ref (fun ?loc n -> anomaly ~label:"detype" (Pp.str "index
 let set_detype_anonymous f = detype_anonymous := f
 
 let detype_level sigma l =
-  let l = Pp.string_of_ppcmds (Termops.pr_evd_level sigma l) in
-  GType (Some (Loc.tag @@ Name.mk_name (Id.of_string_soft l)))
+  let l = Termops.reference_of_level sigma l in
+  GType (UNamed l)
 
 let detype_instance sigma l = 
   let l = EInstance.kind sigma l in
diff --git a/pretyping/miscops.ml b/pretyping/miscops.ml
index bc563b46d..f0cb8fd1f 100644
--- a/pretyping/miscops.ml
+++ b/pretyping/miscops.ml
@@ -30,7 +30,8 @@ let smartmap_cast_type f c =
 let glob_sort_eq g1 g2 = match g1, g2 with
 | GProp, GProp -> true
 | GSet, GSet -> true
-| GType l1, GType l2 -> List.equal (fun x y -> Names.Name.equal (snd x) (snd y)) l1 l2
+| GType l1, GType l2 ->
+   List.equal (Option.equal (fun (x,m) (y,n) -> Libnames.eq_reference x y && Int.equal m n)) l1 l2
 | _ -> false
 
 let intro_pattern_naming_eq nam1 nam2 = match nam1, nam2 with
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 00c254dbe..b930c5db8 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -177,61 +177,77 @@ let _ =
 	    optwrite = (:=) Universes.set_minimization })
 
 (** Miscellaneous interpretation functions *)
-let interp_known_universe_level evd id =
+
+let interp_known_universe_level evd r =
+  let loc, qid = Libnames.qualid_of_reference r in
   try
-    let level = Evd.universe_of_name evd id in
-    level
+    match r with
+    | Libnames.Ident (loc, id) -> Evd.universe_of_name evd id
+    | Libnames.Qualid _ -> raise Not_found
   with Not_found ->
-    let names, _ = Global.global_universe_names () in
-    snd (Id.Map.find id names)
-
-let interp_universe_level_name ~anon_rigidity evd (loc, s) =
-  match s with
-  | Anonymous ->
-     new_univ_level_variable ?loc anon_rigidity evd
-  | Name id ->
-     let s = Id.to_string id in
-     if CString.string_contains ~where:s ~what:"." then
-       match List.rev (CString.split '.' s) with
-       | [] -> anomaly (str"Invalid universe name " ++ str s ++ str".")
-       | n :: dp ->
-	  let num = int_of_string n in
-	  let dp = DirPath.make (List.map Id.of_string dp) in
-	  let level = Univ.Level.make dp num in
-	  let evd =
-	    try Evd.add_global_univ evd level
-	    with UGraph.AlreadyDeclared -> evd
-	  in evd, level
-     else
-       try evd, interp_known_universe_level evd id
-       with Not_found ->
-         if not (is_strict_universe_declarations ()) then
-           new_univ_level_variable ?loc ~name:id univ_rigid evd
-         else user_err ?loc ~hdr:"interp_universe_level_name"
-             (Pp.(str "Undeclared universe: " ++ str s))
+    let univ, k = Nametab.locate_universe qid in
+    Univ.Level.make univ k
+
+let interp_universe_level_name ~anon_rigidity evd r =
+  try evd, interp_known_universe_level evd r
+  with Not_found ->
+    match r with (* Qualified generated name *)
+    | Libnames.Qualid (loc, qid) ->
+       let dp, i = Libnames.repr_qualid qid in
+       let num =
+         try int_of_string (Id.to_string i)
+         with Failure _ ->
+           user_err ?loc ~hdr:"interp_universe_level_name"
+                    (Pp.(str "Undeclared global universe: " ++ Libnames.pr_reference r))
+       in
+       let level = Univ.Level.make dp num in
+       let evd =
+         try Evd.add_global_univ evd level
+         with UGraph.AlreadyDeclared -> evd
+       in evd, level
+    | Libnames.Ident (loc, id) -> (* Undeclared *)
+        if not (is_strict_universe_declarations ()) then
+          new_univ_level_variable ?loc ~name:id univ_rigid evd
+        else user_err ?loc ~hdr:"interp_universe_level_name"
+                      (Pp.(str "Undeclared universe: " ++ Id.print id))
 
 let interp_universe ?loc evd = function
   | [] -> let evd, l = new_univ_level_variable ?loc univ_rigid evd in
 	    evd, Univ.Universe.make l
   | l ->
-    List.fold_left (fun (evd, u) l -> 
-        (* [univ_flexible_alg] can produce algebraic universes in terms *)
-        let evd', l = interp_universe_level_name ~anon_rigidity:univ_flexible evd l in
-	(evd', Univ.sup u (Univ.Universe.make l)))
+    List.fold_left (fun (evd, u) l ->
+      let evd', u' =
+        match l with
+        | Some (l,n) ->
+           (* [univ_flexible_alg] can produce algebraic universes in terms *)
+           let anon_rigidity = univ_flexible in
+           let evd', l = interp_universe_level_name ~anon_rigidity evd l in
+           let u' = Univ.Universe.make l in
+           (match n with
+            | 0 -> evd', u'
+            | 1 -> evd', Univ.Universe.super u'
+            | _ ->
+               user_err ?loc ~hdr:"interp_universe"
+                        (Pp.(str "Cannot interpret universe increment +" ++ int n)))
+        | None ->
+           let evd, l = new_univ_level_variable ?loc univ_flexible evd in
+           evd, Univ.Universe.make l
+      in (evd', Univ.sup u u'))
     (evd, Univ.Universe.type0m) l
 
 let interp_known_level_info ?loc evd = function
-  | None | Some (_, Anonymous) ->
+  | UUnknown | UAnonymous ->
     user_err ?loc ~hdr:"interp_known_level_info"
       (str "Anonymous universes not allowed here.")
-  | Some (loc, Name id) ->
-    try interp_known_universe_level evd id
+  | UNamed ref ->
+    try interp_known_universe_level evd ref
     with Not_found ->
-      user_err ?loc ~hdr:"interp_known_level_info" (str "Undeclared universe " ++ Id.print id)
+      user_err ?loc ~hdr:"interp_known_level_info" (str "Undeclared universe " ++ Libnames.pr_reference ref)
 
 let interp_level_info ?loc evd : Misctypes.level_info -> _ = function
-  | None -> new_univ_level_variable ?loc univ_rigid evd
-  | Some (loc,s) -> interp_universe_level_name ~anon_rigidity:univ_flexible evd (Loc.tag ?loc s)
+  | UUnknown -> new_univ_level_variable ?loc univ_rigid evd
+  | UAnonymous -> new_univ_level_variable ?loc univ_flexible evd
+  | UNamed s -> interp_universe_level_name ~anon_rigidity:univ_flexible evd s
 
 type inference_hook = env -> evar_map -> Evar.t -> evar_map * constr