let disambiguate_term ~context ~metasenv ~subst ~expty
?(initial_ugraph = CicUniv.oblivion_ugraph)
- ~mk_implicit ~description_of_alias ~mk_choice
+ ~mk_implicit ~description_of_alias ~fix_instance ~mk_choice
~aliases ~universe ~lookup_in_library (text,prefix_len,term)
=
let mk_localization_tbl x = Cic.CicHash.create x in
MultiPassDisambiguator.disambiguate_thing ~context ~metasenv ~subst
~initial_ugraph ~aliases ~string_context_of_context
~universe ~lookup_in_library ~mk_implicit ~description_of_alias
+ ~fix_instance
~uri:None ~pp_thing:CicNotationPp.pp_term
~domain_of_thing:Disambiguate.domain_of_term
~interpretate_thing:(interpretate_term (?create_dummy_ids:None) ~mk_choice)
~freshen_thing:CicNotationUtil.freshen_term
~passes:(MultiPassDisambiguator.passes ())
-let disambiguate_obj ~mk_implicit ~description_of_alias ~mk_choice
+let disambiguate_obj ~mk_implicit ~description_of_alias ~fix_instance ~mk_choice
~aliases ~universe ~lookup_in_library ~uri (text,prefix_len,obj)
=
let mk_localization_tbl x = Cic.CicHash.create x in
~aliases ~universe ~uri ~string_context_of_context
~pp_thing:(CicNotationPp.pp_obj CicNotationPp.pp_term)
~domain_of_thing:Disambiguate.domain_of_obj
- ~lookup_in_library ~mk_implicit ~description_of_alias
+ ~lookup_in_library ~mk_implicit ~description_of_alias ~fix_instance
~initial_ugraph:CicUniv.empty_ugraph
~interpretate_thing:(interpretate_obj ~mk_choice)
~refine_thing:refine_obj