Univs: local names handling.

Keep user-side information on the names used in instances of universe
polymorphic references and use them for printing.

2 files changed, 25 insertions, 1 deletions

diff --git a/library/universes.ml b/library/universes.ml
index 30d38eb2a4..6cccb10efb 100644
--- a/library/universes.ml
+++ b/library/universes.ml
@@ -12,7 +12,9 @@ open Names
 open Term
 open Environ
 open Univ
+open Globnames
 
+(** Global universe names *)
 type universe_names = 
     Univ.universe_level Idmap.t * Id.t Univ.LMap.t
 
@@ -27,6 +29,20 @@ let pr_with_global_universes l =
   try Nameops.pr_id (LMap.find l (snd !global_universes))
   with Not_found -> Level.pr l
 
+(** Local universe names of polymorphic references *)
+
+type universe_binders = (Id.t * Univ.universe_level) list
+
+let universe_binders_table = Summary.ref Refmap.empty ~name:"universe binders"
+
+let universe_binders_of_global ref =
+  try
+    let l = Refmap.find ref !universe_binders_table in l
+  with Not_found -> []
+
+let register_universe_binders ref l =
+  universe_binders_table := Refmap.add ref l !universe_binders_table
+		     
 (* To disallow minimization to Set *)
 
 let set_minimization = ref true
diff --git a/library/universes.mli b/library/universes.mli
index 4ff21d45c9..45672ef460 100644
--- a/library/universes.mli
+++ b/library/universes.mli
@@ -14,9 +14,10 @@ open Univ
 
 val set_minimization : bool ref
 val is_set_minimization : unit -> bool
-       
+
 (** Universes *)
 
+(** Global universe name <-> level mapping *)
 type universe_names = 
   Univ.universe_level Idmap.t * Id.t Univ.LMap.t
 
@@ -25,6 +26,13 @@ val set_global_universe_names : universe_names -> unit
 
 val pr_with_global_universes : Level.t -> Pp.std_ppcmds
 
+(** Local universe name <-> level mapping *)
+
+type universe_binders = (Id.t * Univ.universe_level) list
+					   
+val register_universe_binders : Globnames.global_reference -> universe_binders -> unit
+val universe_binders_of_global : Globnames.global_reference -> universe_binders
+
 (** The global universe counter *)
 val set_remote_new_univ_level : universe_level RemoteCounter.installer