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