let (annobj, _, _, ids_to_inner_sorts, _, _, _) =
Cic2acic.acic_object_of_cic_object ~eta_fix:false obj
in
let (annobj, _, _, ids_to_inner_sorts, _, _, _) =
Cic2acic.acic_object_of_cic_object ~eta_fix:false obj
in
in
let new_pp = BoxPp.pp_term ast in
debug_print ("ast:\n" ^ new_pp);
let new_ast = CicTextualParser2.parse_term (Stream.of_string new_pp) in
debug_print ("new_ast:\n" ^ CicAstPp.pp_term ast);
let res =
in
let new_pp = BoxPp.pp_term ast in
debug_print ("ast:\n" ^ new_pp);
let new_ast = CicTextualParser2.parse_term (Stream.of_string new_pp) in
debug_print ("new_ast:\n" ^ CicAstPp.pp_term ast);
let res =
- Disambiguate'.disambiguate_term mqi_handle [] [] new_ast
- DisambiguateTypes.Environment.empty in
+ Disambiguate'.disambiguate_term ~dbd [] [] new_ast
+ ~aliases:DisambiguateTypes.Environment.empty
+ ~initial_ugraph:CicUniv.empty_ugraph
+ in
debug_print
("domain: " ^ CicTextualParser2.EnvironmentP3.to_string domain) ;
debug_print ("term: " ^ CicPp.ppterm term)
debug_print
("domain: " ^ CicTextualParser2.EnvironmentP3.to_string domain) ;
debug_print ("term: " ^ CicPp.ppterm term)