val interpretate_path :
context:Cic.name list -> CicNotationPt.term -> Cic.term
-module type CicDisambiguator =
-sig
- val disambiguate_term :
- ?fresh_instances:bool ->
- context:Cic.context ->
- metasenv:Cic.metasenv ->
- subst:Cic.substitution ->
- ?goal:int ->
- ?initial_ugraph:CicUniv.universe_graph ->
- aliases:Cic.term DisambiguateTypes.environment ->
- universe:Cic.term DisambiguateTypes.multiple_environment 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) ->
- CicNotationPt.term Disambiguate.disambiguator_input ->
- ((DisambiguateTypes.domain_item *
- Cic.term DisambiguateTypes.codomain_item) list *
- Cic.metasenv *
- Cic.substitution *
- Cic.term*
- CicUniv.universe_graph) list *
- bool
+val disambiguate_term :
+ context:Cic.context ->
+ metasenv:Cic.metasenv ->
+ subst:Cic.substitution ->
+ ?goal:int ->
+ ?initial_ugraph:CicUniv.universe_graph ->
+ 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 ->
+ 'alias list) ->
+ CicNotationPt.term Disambiguate.disambiguator_input ->
+ ((DisambiguateTypes.domain_item * 'alias) list *
+ Cic.metasenv *
+ Cic.substitution *
+ Cic.term*
+ CicUniv.universe_graph) list *
+ bool
- val disambiguate_obj :
- ?fresh_instances:bool ->
- aliases:Cic.term DisambiguateTypes.environment ->
- universe:Cic.term DisambiguateTypes.multiple_environment option ->
- uri:UriManager.uri option -> (* required only for inductive types *)
- lookup_in_library:(
- DisambiguateTypes.interactive_user_uri_choice_type ->
- DisambiguateTypes.input_or_locate_uri_type ->
- DisambiguateTypes.Environment.key ->
- Cic.term DisambiguateTypes.codomain_item list) ->
- CicNotationPt.term CicNotationPt.obj Disambiguate.disambiguator_input ->
- ((DisambiguateTypes.domain_item *
- Cic.term DisambiguateTypes.codomain_item) list *
- Cic.metasenv *
- Cic.substitution *
- Cic.obj *
- CicUniv.universe_graph) list *
- bool
-end
-
-module Make (C : DisambiguateTypes.Callbacks) : CicDisambiguator
+val disambiguate_obj :
+ 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 ->
+ 'alias list) ->
+ uri:UriManager.uri option -> (* required only for inductive types *)
+ CicNotationPt.term CicNotationPt.obj Disambiguate.disambiguator_input ->
+ ((DisambiguateTypes.domain_item * 'alias) list *
+ Cic.metasenv *
+ Cic.substitution *
+ Cic.obj *
+ CicUniv.universe_graph) list *
+ bool