subst:Cic.substitution ->
?goal:int ->
?initial_ugraph:CicUniv.universe_graph ->
- aliases:Cic.term DisambiguateTypes.environment ->
- universe:Cic.term DisambiguateTypes.multiple_environment option ->
+ mk_implicit:(bool -> 'alias) ->
+ description_of_alias:('alias -> string) ->
+ mk_choice:('alias -> Cic.term DisambiguateTypes.codomain_item) ->
+ aliases:'alias DisambiguateTypes.Environment.t ->
+ universe:'alias list DisambiguateTypes.Environment.t option ->
lookup_in_library:(
DisambiguateTypes.interactive_user_uri_choice_type ->
DisambiguateTypes.input_or_locate_uri_type ->
DisambiguateTypes.Environment.key ->
- Cic.term DisambiguateTypes.codomain_item list) ->
+ 'alias list) ->
CicNotationPt.term Disambiguate.disambiguator_input ->
- ((DisambiguateTypes.domain_item *
- Cic.term DisambiguateTypes.codomain_item) list *
+ ((DisambiguateTypes.domain_item * 'alias) list *
Cic.metasenv *
Cic.substitution *
Cic.term*
bool
val disambiguate_obj :
- aliases:Cic.term DisambiguateTypes.environment ->
- universe:Cic.term DisambiguateTypes.multiple_environment option ->
- uri:UriManager.uri option -> (* required only for inductive types *)
+ mk_implicit:(bool -> 'alias) ->
+ description_of_alias:('alias -> string) ->
+ mk_choice:('alias -> Cic.term DisambiguateTypes.codomain_item) ->
+ aliases:'alias DisambiguateTypes.Environment.t ->
+ universe:'alias list DisambiguateTypes.Environment.t option ->
lookup_in_library:(
DisambiguateTypes.interactive_user_uri_choice_type ->
DisambiguateTypes.input_or_locate_uri_type ->
DisambiguateTypes.Environment.key ->
- Cic.term DisambiguateTypes.codomain_item list) ->
+ 'alias list) ->
+ uri:UriManager.uri option -> (* required only for inductive types *)
CicNotationPt.term CicNotationPt.obj Disambiguate.disambiguator_input ->
- ((DisambiguateTypes.domain_item *
- Cic.term DisambiguateTypes.codomain_item) list *
+ ((DisambiguateTypes.domain_item * 'alias) list *
Cic.metasenv *
Cic.substitution *
Cic.obj *