Stop calling Id.Map.domain on univ binders every individual universe

2 files changed, 11 insertions, 4 deletions

diff --git a/library/nametab.ml b/library/nametab.ml
index d5cc4f8ac5..e94b696b60 100644
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -98,6 +98,7 @@ module type NAMETREE = sig
   val find : user_name -> t -> elt
   val exists : user_name -> t -> bool
   val user_name : qualid -> t -> user_name
+  val shortest_qualid_gen : ?loc:Loc.t -> (Id.t -> bool) -> user_name -> t -> qualid
   val shortest_qualid : ?loc:Loc.t -> Id.Set.t -> user_name -> t -> qualid
   val find_prefixes : qualid -> t -> elt list
 
@@ -252,9 +253,9 @@ let exists uname tab =
   with
       Not_found -> false
 
-let shortest_qualid ?loc ctx uname tab =
+let shortest_qualid_gen ?loc hidden uname tab =
   let id,dir = U.repr uname in
-  let hidden = Id.Set.mem id ctx in
+  let hidden = hidden id in
   let rec find_uname pos dir tree =
     let is_empty = match pos with [] -> true | _ -> false in
     match tree.path with
@@ -269,6 +270,9 @@ let shortest_qualid ?loc ctx uname tab =
   let found_dir = find_uname [] dir ptab in
     make_qualid ?loc (DirPath.make found_dir) id
 
+let shortest_qualid ?loc ctx uname tab =
+  shortest_qualid_gen ?loc (fun id -> Id.Set.mem id ctx) uname tab
+
 let push_node node l =
   match node with
   | Absolute (_,o) | Relative (_,o) when not (List.mem_f E.equal o l) -> o::l
@@ -564,7 +568,7 @@ let shortest_qualid_of_modtype ?loc kn =
 
 let shortest_qualid_of_universe ?loc ctx kn =
   let sp = UnivIdMap.find kn !the_univrevtab in
-    UnivTab.shortest_qualid ?loc ctx sp !the_univtab
+    UnivTab.shortest_qualid_gen ?loc (fun id -> Id.Map.mem id ctx) sp !the_univtab
 
 let pr_global_env env ref =
   try pr_qualid (shortest_qualid_of_global env ref)
diff --git a/library/nametab.mli b/library/nametab.mli
index fa27dcab9a..33aebca0b9 100644
--- a/library/nametab.mli
+++ b/library/nametab.mli
@@ -206,7 +206,9 @@ val shortest_qualid_of_global : ?loc:Loc.t -> Id.Set.t -> GlobRef.t -> qualid
 val shortest_qualid_of_syndef : ?loc:Loc.t -> Id.Set.t -> syndef_name -> qualid
 val shortest_qualid_of_modtype : ?loc:Loc.t -> ModPath.t -> qualid
 val shortest_qualid_of_module : ?loc:Loc.t -> ModPath.t -> qualid
-val shortest_qualid_of_universe : ?loc:Loc.t -> Id.Set.t -> Univ.Level.UGlobal.t -> qualid
+
+(** In general we have a [UnivNames.universe_binders] around rather than a [Id.Set.t] *)
+val shortest_qualid_of_universe : ?loc:Loc.t -> 'u Id.Map.t -> Univ.Level.UGlobal.t -> qualid
 
 (** {5 Generic name handling} *)
 
@@ -236,6 +238,7 @@ module type NAMETREE = sig
   val find : user_name -> t -> elt
   val exists : user_name -> t -> bool
   val user_name : qualid -> t -> user_name
+  val shortest_qualid_gen : ?loc:Loc.t -> (Id.t -> bool) -> user_name -> t -> qualid
   val shortest_qualid : ?loc:Loc.t -> Id.Set.t -> user_name -> t -> qualid
   val find_prefixes : qualid -> t -> elt list
   val match_prefixes : qualid -> t -> elt list