let refine_profiler = HExtlib.profile "disambiguate_thing.refine_thing"
+type alias_spec =
+ | Ident_alias of string * string (* identifier, uri *)
+ | Symbol_alias of string * int * string (* name, instance no, description *)
+ | Number_alias of int * string (* instance no, description *)
+
let disambiguate_thing
~context ~metasenv ~subst ~use_coercions
~string_context_of_context
~initial_ugraph:base_univ ~expty
- ~mk_implicit ~description_of_alias
+ ~mk_implicit ~description_of_alias ~fix_instance
~aliases ~universe ~lookup_in_library
~uri ~pp_thing ~domain_of_thing ~interpretate_thing ~refine_thing
~mk_localization_tbl
input_or_locate_uri item
| Some e ->
(try
- let item =
- match item with
- | Symbol (symb, _) -> Symbol (symb, 0)
- | item -> item
- in
- Environment.find item e
+ fix_instance item (Environment.find item e)
with Not_found -> [])
in
(*