diff options
Diffstat (limited to 'library/nametab.ml')
| -rw-r--r-- | library/nametab.ml | 10 |
1 files changed, 7 insertions, 3 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) |