module Make (C : DisambiguateTypes.Callbacks) : sig
val disambiguate_term :
?fresh_instances:bool ->
- dbd:HSql.dbd ->
context:NCic.context ->
metasenv:NCic.metasenv ->
subst:NCic.substitution ->
- aliases:DisambiguateTypes.environment ->(* previous interpretation status *)
- universe:DisambiguateTypes.multiple_environment option ->
+ aliases:NCic.term DisambiguateTypes.environment ->(* previous interpretation status *)
+ universe:NCic.term DisambiguateTypes.multiple_environment option ->
+ lookup_in_library:((selection_mode:[ `MULTIPLE | `SINGLE ] ->
+ ?ok:string ->
+ ?enable_button_for_non_vars:bool ->
+ title:string ->
+ msg:string ->
+ id:string ->
+ UriManager.uri list -> UriManager.uri list) ->
+ (title:string -> ?id:string -> unit -> UriManager.uri option) ->
+ DisambiguateTypes.Environment.key ->
+ NCic.term DisambiguateTypes.codomain_item list) ->
?goal: int ->
CicNotationPt.term Disambiguate.disambiguator_input ->
- ((DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list *
+ ((DisambiguateTypes.domain_item * NCic.term DisambiguateTypes.codomain_item) list *
NCic.metasenv * (* new metasenv *)
NCic.substitution *
NCic.term) list * (* disambiguated term *)