- debug_print ("ast: " ^ CicAstPp.pp_term ast);
- let (_, _, term) =
- Disambiguate'.disambiguate_term mqi_handle [] [] ast
- DisambiguateTypes.Environment.empty
- in
- debug_print ("term: " ^ CicPp.ppterm term)
+ 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
+ List.iter
+ (fun (domain, _, term) ->
+ debug_print
+ ("domain: " ^ CicTextualParser2.EnvironmentP3.to_string domain) ;
+ debug_print ("term: " ^ CicPp.ppterm term)
+ ) res ;
+ List.length res