(Ok (term', metasenv')),ugraph1
with
| CicRefine.Uncertain _ ->
- debug_print ("%%% UNCERTAIN!!! " ^ CicPp.ppterm term) ;
+ debug_print ("UNCERTAIN!!! " ^ CicPp.ppterm term) ;
Uncertain,ugraph
- | CicRefine.RefineFailure _ ->
- debug_print ("%%% PRUNED!!! " ^ CicPp.ppterm term) ;
+ | CicRefine.RefineFailure msg ->
+ debug_print (sprintf "PRUNED!!!\nterm%s\nmessage:%s"
+ (CicPp.ppterm term) msg);
Ko,ugraph
| CicUnification.UnificationFailure s ->
prerr_endline ("PASSADI QUI: " ^ s);
let resolve (env: environment) (item: domain_item) ?(num = "") ?(args = []) () =
try
snd (Environment.find item env) env num args
- with Not_found -> assert false
+ with Not_found ->
+ failwith ("Domain item not found: " ^
+ (DisambiguateTypes.string_of_domain_item item))
(* TODO move it to Cic *)
let find_in_environment name context =
uris
let disambiguate_term ~(dbd:Mysql.dbd) context metasenv term
- ?(initial_ugraph = CicUniv.empty_ugraph) ~aliases:current_env
+ ?(initial_ugraph = CicUniv.empty_ugraph) ~aliases:current_env
=
debug_print "NEW DISAMBIGUATE INPUT";
let disambiguate_context = (* cic context -> disambiguate context *)