'metasenv -> 'subst -> 'context -> 'uri -> use_coercions:bool ->
'raw_thing -> 'ugraph -> localization_tbl:'cichash ->
('refined_thing, 'metasenv,'subst,'ugraph) test_result) ->
- localization_tbl:'cichash ->
+ mk_localization_tbl:(int -> 'cichash) ->
string * int * 'ast_thing ->
((DisambiguateTypes.Environment.key * 'alias) list *
'metasenv * 'subst * 'refined_thing * 'ugraph)
~mk_implicit ~description_of_alias
~aliases ~universe ~lookup_in_library
~uri ~pp_thing ~domain_of_thing ~interpretate_thing ~refine_thing
- ~localization_tbl
+ ~mk_localization_tbl
(thing_txt,thing_txt_prefix_len,thing)
=
debug_print (lazy "DISAMBIGUATE INPUT");
env in
aux (aux env l) tl in
let filled_env = aux aliases todo_dom in
+ let localization_tbl = mk_localization_tbl 503 in
let cic_thing =
interpretate_thing ~context ~env:filled_env
~uri ~is_path:false thing ~localization_tbl
(inner_dom@remaining_dom@rem_dom) base_univ
with
| Ok (thing, metasenv,subst,new_univ) ->
+(* prerr_endline "OK"; *)
let res =
(match inner_dom with
| [] ->
in
res @@ filter tl
| Uncertain loc_msg ->
+(* prerr_endline ("UNCERTAIN"); *)
let res =
(match inner_dom with
| [] -> [],[new_env,new_diff,loc_msg],[]
in
res @@ filter tl
| Ko loc_msg ->
+(* prerr_endline "KO"; *)
let res = [],[],[new_env,new_diff,loc_msg,true] in
res @@ filter tl)
in