3 module Make (C : DisambiguateTypes.Callbacks) : sig
4 val disambiguate_term :
5 ?fresh_instances:bool ->
7 context:NCic.context ->
8 metasenv:NCic.metasenv ->
9 aliases:DisambiguateTypes.environment ->(* previous interpretation status *)
10 universe:DisambiguateTypes.multiple_environment option ->
11 CicNotationPt.term Disambiguate.disambiguator_input ->
12 ((DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list *
13 NCic.metasenv * (* new metasenv *)
14 NCic.term) list * (* disambiguated term *)