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, 15 insertions, 5 deletions

diff --git a/engine/universes.mli b/engine/universes.mli
index 1401c4ee8..fc9278eb5 100644
--- a/engine/universes.mli
+++ b/engine/universes.mli
@@ -18,6 +18,13 @@ val is_set_minimization : unit -> bool
 (** Universes *)
 
 val pr_with_global_universes : Level.t -> Pp.t
+val reference_of_level : Level.t -> Libnames.reference
+
+(** Global universe information outside the kernel, to handle
+    polymorphic universes in sections that have to be discharged. *)
+val add_global_universe : Level.t -> Decl_kinds.polymorphic -> unit
+
+val is_polymorphic : Level.t -> bool
 
 (** Local universe name <-> level mapping *)
 
@@ -40,14 +47,17 @@ val universe_binders_with_opt_names : Globnames.global_reference ->
   Univ.Level.t list -> univ_name_list option -> universe_binders
 
 (** The global universe counter *)
-val set_remote_new_univ_level : Level.t RemoteCounter.installer
+type universe_id = DirPath.t * int
+
+val set_remote_new_univ_id : universe_id RemoteCounter.installer
 
 (** Side-effecting functions creating new universe levels. *)
 
-val new_univ_level : DirPath.t -> Level.t
-val new_univ : DirPath.t -> Universe.t
-val new_Type : DirPath.t -> types
-val new_Type_sort : DirPath.t -> Sorts.t
+val new_univ_id : unit -> universe_id
+val new_univ_level : unit -> Level.t
+val new_univ : unit -> Universe.t
+val new_Type : unit -> types
+val new_Type_sort : unit -> Sorts.t
 
 val new_global_univ : unit -> Universe.t in_universe_context_set
 val new_sort_in_family : Sorts.family -> Sorts.t