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 (_, _, term) =
- Disambiguate'.disambiguate_term mqi_handle [] [] new_ast
- DisambiguateTypes.Environment.empty
- in
- debug_print ("term: " ^ CicPp.ppterm term)
+ List.iter
+ (fun (_, _, term) ->
+ debug_print ("term: " ^ CicPp.ppterm term))
+ (Disambiguate'.disambiguate_term mqi_handle [] [] new_ast
+ DisambiguateTypes.Environment.empty)
in
match annobj with
| Cic.AConstant (_, _, _, None, ty, _) ->