exception NoWellTypedInterpretation of
int *
((Stdpp.location list * string * string) list *
- (DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list *
- (Stdpp.location * string) Lazy.t * bool) list
+ (DisambiguateTypes.domain_item * string) list *
+ (Stdpp.location * string) Lazy.t *
+ bool) list
exception PathNotWellFormed
val interpretate_path :
module type Disambiguator =
sig
val disambiguate_thing:
- dbd:HSql.dbd ->
context:'context ->
metasenv:'metasenv ->
subst:'subst ->
+ mk_implicit:([ `Closed ] option -> 'refined_thing) ->
initial_ugraph:'ugraph ->
hint: ('metasenv -> 'raw_thing -> 'raw_thing) *
(('refined_thing,'metasenv,'subst,'ugraph) test_result ->
('refined_thing,'metasenv,'subst,'ugraph) test_result) ->
- aliases:DisambiguateTypes.codomain_item DisambiguateTypes.Environment.t ->
- universe:DisambiguateTypes.codomain_item list
+ aliases:'refined_thing DisambiguateTypes.codomain_item DisambiguateTypes.Environment.t ->
+ universe:'refined_thing DisambiguateTypes.codomain_item list
DisambiguateTypes.Environment.t 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 ->
+ 'refined_thing DisambiguateTypes.codomain_item list) ->
uri:'uri ->
pp_thing:('ast_thing -> string) ->
domain_of_thing:(context:'context -> 'ast_thing -> domain) ->
interpretate_thing:(context:'context ->
- env:DisambiguateTypes.codomain_item
+ env:'refined_thing DisambiguateTypes.codomain_item
DisambiguateTypes.Environment.t ->
uri:'uri ->
is_path:bool -> 'ast_thing -> localization_tbl:'cichash -> 'raw_thing) ->
('refined_thing, 'metasenv,'subst,'ugraph) test_result) ->
localization_tbl:'cichash ->
string * int * 'ast_thing ->
- ((DisambiguateTypes.Environment.key * DisambiguateTypes.codomain_item)
- list * 'metasenv * 'subst * 'refined_thing * 'ugraph)
- list * bool
+ ((DisambiguateTypes.Environment.key *
+ 'refined_thing DisambiguateTypes.codomain_item) list *
+ 'metasenv * 'subst * 'refined_thing * 'ugraph)
+ list * bool
val disambiguate_term :
?fresh_instances:bool ->
- dbd:HSql.dbd ->
context:Cic.context ->
metasenv:Cic.metasenv ->
subst:Cic.substitution ->
?goal:int ->
?initial_ugraph:CicUniv.universe_graph ->
- aliases:DisambiguateTypes.environment ->(* previous interpretation status *)
- universe:DisambiguateTypes.multiple_environment option ->
+ aliases:Cic.term DisambiguateTypes.environment ->(* previous interpretation status *)
+ universe:Cic.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 ->
+ Cic.term DisambiguateTypes.codomain_item list) ->
CicNotationPt.term disambiguator_input ->
- ((DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list *
+ ((DisambiguateTypes.domain_item * Cic.term DisambiguateTypes.codomain_item) list *
Cic.metasenv * (* new metasenv *)
Cic.substitution *
Cic.term*
val disambiguate_obj :
?fresh_instances:bool ->
- dbd:HSql.dbd ->
- aliases:DisambiguateTypes.environment ->(* previous interpretation status *)
- universe:DisambiguateTypes.multiple_environment option ->
+ aliases:Cic.term DisambiguateTypes.environment ->(* previous interpretation status *)
+ universe:Cic.term DisambiguateTypes.multiple_environment option ->
uri:UriManager.uri option -> (* required only for inductive types *)
+ 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 ->
+ Cic.term DisambiguateTypes.codomain_item list) ->
CicNotationPt.term CicNotationPt.obj disambiguator_input ->
- ((DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list *
+ ((DisambiguateTypes.domain_item * Cic.term DisambiguateTypes.codomain_item) list *
Cic.metasenv * (* new metasenv *)
Cic.substitution *
Cic.obj *