module Make (C : DisambiguateTypes.Callbacks) : sig
val disambiguate_term :
    ?fresh_instances:bool ->
    dbd:HSql.dbd ->
    context:NCic.context ->
    metasenv:NCic.metasenv ->
    aliases:DisambiguateTypes.environment ->(* previous interpretation status *)
    universe:DisambiguateTypes.multiple_environment option ->
    CicNotationPt.term Disambiguate.disambiguator_input ->
    ((DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list *
     NCic.metasenv *                  (* new metasenv *)
     NCic.term) list *  (* disambiguated term *)
    bool
end