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.

1 files changed, 4 insertions, 18 deletions

diff --git a/kernel/univ.mli b/kernel/univ.mli
index 69aecac4f3..512f38cedd 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -12,20 +12,10 @@
 module Level :
 sig
 
-  module Id : sig
+  module UGlobal : sig
     type t
 
-    val make : int -> t
-    val to_string : t -> string
-
-  end
-  (** Non-qualified global universe level *)
-
-  module Qualid : sig
-    type t
-
-    val make : Names.DirPath.t -> Id.t -> t
-    val repr : t -> Names.DirPath.t * Id.t
+    val make : Names.DirPath.t -> int -> t
     val equal : t -> t -> bool
     val hash : t -> int
     val compare : t -> t -> int
@@ -57,11 +47,7 @@ sig
 
   val hash : t -> int
 
-  val make : Qualid.t -> t
-
-  val make2 : Names.DirPath.t -> Id.t -> t
-  (** Create a new universe level from a unique identifier and an associated
-      module path. *)
+  val make : UGlobal.t -> t
 
   val pr : t -> Pp.t
   (** Pretty-printing *)
@@ -73,7 +59,7 @@ sig
 
   val var_index : t -> int option
 
-  val name : t -> Qualid.t option
+  val name : t -> UGlobal.t option
 end
 
 (** Sets of universe levels *)