Revise API for global universes.

Rename Univ.Level.{Qualid -> UGlobal}, remove Univ.Level.Id.

Remove the ability to split the argument of `Univ.Level.Level` into a
dirpath*int pair (except by going through string hacks like
detyping/pretyping(/funind) does).

Id.of_string_soft to turn unnamed universes into qualid is pushed up
to detyping. (TODO some followup PR clean up more)

This makes it pointless to have an opaque type for ints in
Univ.Level: it would only be used as argument to
Univ.Level.UGlobal.make, ie
~~~
open Univ.Level
let x = UGlobal.make dp (Id.make n)
(* vs *)
let x = UGlobal.make dp n
~~~

Remaining places which create levels from ints are various hacks (eg
the dummy in inductive.ml, the Type.n universes in ugraph
sort_universes) and univgen.

UnivGen does have an opaque type for ints used as univ ids since they
get manipulated by the stm.

NB: build breaks due to ocamldep issue if UGlobal is named Global instead.

7 files changed, 24 insertions, 20 deletions

diff --git a/engine/termops.mli b/engine/termops.mli
index eef8452e64..7920af8e0e 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -290,7 +290,7 @@ val is_Prop : Evd.evar_map -> constr -> bool
 val is_Set : Evd.evar_map -> constr -> bool
 val is_Type : Evd.evar_map -> constr -> bool
 
-val reference_of_level : Evd.evar_map -> Univ.Level.t -> Libnames.qualid
+val reference_of_level : Evd.evar_map -> Univ.Level.t -> Libnames.qualid option
 
 (** Combinators on judgments *)
 
diff --git a/engine/uState.ml b/engine/uState.ml
index 56b7a16ace..185283225c 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -324,12 +324,14 @@ let constrain_variables diff ctx =
 let qualid_of_level uctx =
   let map, map_rev = uctx.uctx_names in 
     fun l ->
-      try Libnames.qualid_of_ident (Option.get (Univ.LMap.find l map_rev).uname)
+      try Some (Libnames.qualid_of_ident (Option.get (Univ.LMap.find l map_rev).uname))
       with Not_found | Option.IsNone ->
         UnivNames.qualid_of_level l
 
 let pr_uctx_level uctx l =
-  Libnames.pr_qualid (qualid_of_level uctx l)
+  match qualid_of_level uctx l with
+  | Some qid -> Libnames.pr_qualid qid
+  | None -> Univ.Level.pr l
 
 type ('a, 'b) gen_universe_decl = {
   univdecl_instance : 'a; (* Declared universes *)
diff --git a/engine/uState.mli b/engine/uState.mli
index ad0cd5c1bb..5170184ef4 100644
--- a/engine/uState.mli
+++ b/engine/uState.mli
@@ -188,6 +188,6 @@ val update_sigma_env : t -> Environ.env -> t
 (** {5 Pretty-printing} *)
 
 val pr_uctx_level : t -> Univ.Level.t -> Pp.t
-val qualid_of_level : t -> Univ.Level.t -> Libnames.qualid
+val qualid_of_level : t -> Univ.Level.t -> Libnames.qualid option
 
 val pr_weak : (Univ.Level.t -> Pp.t) -> t -> Pp.t
diff --git a/engine/univGen.ml b/engine/univGen.ml
index 5aa4734b23..40c4c909fe 100644
--- a/engine/univGen.ml
+++ b/engine/univGen.ml
@@ -13,14 +13,17 @@ open Names
 open Constr
 open Univ
 
+type univ_unique_id = int
 (* Generator of levels *)
 let new_univ_id, set_remote_new_univ_id =
   RemoteCounter.new_counter ~name:"Universes" 0 ~incr:((+) 1)
-    ~build:(fun n -> Level.Id.make n)
+    ~build:(fun n -> n)
+
+let new_univ_global () =
+  Univ.Level.UGlobal.make (Global.current_dirpath ()) (new_univ_id ())
 
 let fresh_level () =
-  let id = new_univ_id () in
-  Univ.Level.make2 (Global.current_dirpath ()) id
+  Univ.Level.make (new_univ_global ())
 
 (* TODO: remove *)
 let new_univ () = Univ.Universe.make (fresh_level ())
diff --git a/engine/univGen.mli b/engine/univGen.mli
index 66e80368a4..b4598e10d0 100644
--- a/engine/univGen.mli
+++ b/engine/univGen.mli
@@ -15,11 +15,13 @@ open Univ
 
 
 (** The global universe counter *)
-val set_remote_new_univ_id : Level.Id.t RemoteCounter.installer
+type univ_unique_id
+val set_remote_new_univ_id : univ_unique_id RemoteCounter.installer
+val new_univ_id : unit -> univ_unique_id (** for the stm *)
 
 (** Side-effecting functions creating new universe levels. *)
 
-val new_univ_id : unit -> Level.Id.t
+val new_univ_global : unit -> Level.UGlobal.t
 val fresh_level : unit -> Level.t
 
 val new_univ : unit -> Universe.t
diff --git a/engine/univNames.ml b/engine/univNames.ml
index 6bf1187b65..19705f9d36 100644
--- a/engine/univNames.ml
+++ b/engine/univNames.ml
@@ -16,17 +16,14 @@ open Univ
 let qualid_of_level l =
   match Level.name l with
   | Some qid  ->
-    begin
-    try Nametab.shortest_qualid_of_universe qid
-    with Not_found ->
-      let (dp,n) = Level.Qualid.repr qid in
-      let name = Id.of_string_soft (Level.Id.to_string n) in
-      Libnames.make_qualid dp name
-    end
-  | None ->
-    Libnames.qualid_of_ident @@ Id.of_string_soft (Level.to_string l)
+    (try Some (Nametab.shortest_qualid_of_universe qid)
+     with Not_found -> None)
+  | None -> None
 
-let pr_with_global_universes l = Libnames.pr_qualid (qualid_of_level l)
+let pr_with_global_universes l =
+  match qualid_of_level l with
+  | Some qid  -> Libnames.pr_qualid qid
+  | None -> Level.pr l
 
 (** Global universe information outside the kernel, to handle
     polymorphic universe names in sections that have to be discharged. *)
diff --git a/engine/univNames.mli b/engine/univNames.mli
index 6e68153ac2..e9c517babf 100644
--- a/engine/univNames.mli
+++ b/engine/univNames.mli
@@ -11,7 +11,7 @@
 open Univ
 
 val pr_with_global_universes : Level.t -> Pp.t
-val qualid_of_level : Level.t -> Libnames.qualid
+val qualid_of_level : Level.t -> Libnames.qualid option
 
 (** Local universe name <-> level mapping *)