DisambiguateTypes.Environment.key ->
?num:string -> ?args:'term list -> unit -> 'term
-val find_in_context: string -> Cic.name list -> int
-
-val domain_of_ast_term: context:Cic.name list -> CicNotationPt.term -> domain
+val find_in_context: string -> string option list -> int
+val domain_of_ast_term: context:
+ string option list -> CicNotationPt.term -> domain
val domain_of_term: context:
- (Cic.name * 'a) option list -> CicNotationPt.term -> domain
+ string option list -> CicNotationPt.term -> domain
val domain_of_obj:
- context:(Cic.name * 'a) option list ->
- CicNotationPt.term CicNotationPt.obj -> domain
+ context:string option list -> CicNotationPt.term CicNotationPt.obj -> domain
module type Disambiguator =
sig
context:'context ->
metasenv:'metasenv ->
subst:'subst ->
+ use_coercions:bool ->
mk_implicit:(bool -> 'refined_term) ->
+ string_context_of_context:('context -> string option list) ->
initial_ugraph:'ugraph ->
hint:
('metasenv -> 'raw_thing -> 'raw_thing) *
'refined_term DisambiguateTypes.codomain_item list) ->
uri:'uri ->
pp_thing:('ast_thing -> string) ->
- domain_of_thing:(context:'context -> 'ast_thing -> domain) ->
+ domain_of_thing:(context: string option list -> 'ast_thing -> domain) ->
interpretate_thing:(
context:'context ->
env:'refined_term DisambiguateTypes.codomain_item
localization_tbl:'cichash ->
'raw_thing) ->
refine_thing:(
- 'metasenv -> 'subst -> 'context -> 'uri ->
+ 'metasenv -> 'subst -> 'context -> 'uri -> use_coercions:bool ->
'raw_thing -> 'ugraph -> localization_tbl:'cichash ->
('refined_thing, 'metasenv,'subst,'ugraph) test_result) ->
localization_tbl:'cichash ->