aliases:DisambiguateTypes.environment ->(* previous interpretation status *)
universe:DisambiguateTypes.multiple_environment option ->
uri:UriManager.uri option -> (* required only for inductive types *)
- CicNotationPt.obj disambiguator_input ->
+ CicNotationPt.term CicNotationPt.obj disambiguator_input ->
((DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list *
Cic.metasenv * (* new metasenv *)
Cic.obj *
if fresh_instances then CicNotationUtil.freshen_obj obj else obj
in
disambiguate_thing ~dbd ~context:[] ~metasenv:[] ~aliases ~universe ~uri
- ~pp_thing:CicNotationPp.pp_obj ~domain_of_thing:domain_of_obj
+ ~pp_thing:(CicNotationPp.pp_obj CicNotationPp.pp_term) ~domain_of_thing:domain_of_obj
~interpretate_thing:interpretate_obj ~refine_thing:refine_obj
(text,prefix_len,obj)
end