From 20c98eab851210702b39e1c66e005acfc351d8dd Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Fri, 1 Dec 2017 10:11:41 +0100
Subject: 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
---
 intf/misctypes.ml | 12 +++++++++---
 1 file changed, 9 insertions(+), 3 deletions(-)

(limited to 'intf')

diff --git a/intf/misctypes.ml b/intf/misctypes.ml
index 87484ccd50..33e961419d 100644
--- a/intf/misctypes.ml
+++ b/intf/misctypes.ml
@@ -48,13 +48,19 @@ type 'a glob_sort_gen =
   | GProp (** representation of [Prop] literal *)
   | GSet  (** representation of [Set] literal *)
   | GType of 'a (** representation of [Type] literal *)
-type sort_info = Name.t Loc.located list
-type level_info = Name.t Loc.located option
 
-type glob_sort = sort_info glob_sort_gen
+type 'a universe_kind =
+  | UAnonymous
+  | UUnknown
+  | UNamed of 'a
+
+type level_info = Libnames.reference universe_kind
 type glob_level = level_info glob_sort_gen
 type glob_constraint = glob_level * Univ.constraint_type * glob_level
 
+type sort_info = (Libnames.reference * int) option list
+type glob_sort = sort_info glob_sort_gen
+
 (** A synonym of [Evar.t], also defined in Term *)
 
 type existential_key = Evar.t
-- 
cgit v1.2.3