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

4 files changed, 13 insertions, 6 deletions

diff --git a/engine/univNames.ml b/engine/univNames.ml
index f5542cc0f7..215f27f535 100644
--- a/engine/univNames.ml
+++ b/engine/univNames.ml
@@ -15,7 +15,7 @@ open Univ
 let qualid_of_level ctx l =
   match Level.name l with
   | Some qid  ->
-    (try Some (Nametab.shortest_qualid_of_universe (Id.Map.domain ctx) qid)
+    (try Some (Nametab.shortest_qualid_of_universe ctx qid)
      with Not_found -> None)
   | None -> None
 
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
diff --git a/tactics/declareUctx.ml b/tactics/declareUctx.ml
index bca43697cb..6c8bc92865 100644
--- a/tactics/declareUctx.ml
+++ b/tactics/declareUctx.ml
@@ -16,7 +16,7 @@ let name_instance inst =
       assert false
     | Some na ->
       try
-        let qid = Nametab.shortest_qualid_of_universe Names.Id.Set.empty na in
+        let qid = Nametab.shortest_qualid_of_universe Names.Id.Map.empty na in
         Names.Name (Libnames.qualid_basename qid)
       with Not_found ->
         (* Best-effort naming from the string representation of the level.