let goal_proof,goal_ty,real_menv,_ =
(* prerr_endline ("parte la refine per: " ^ (CicPp.pp goal_proof names)); *)
try
debug_print (lazy (CicPp.ppterm goal_proof));
let goal_proof,goal_ty,real_menv,_ =
(* prerr_endline ("parte la refine per: " ^ (CicPp.pp goal_proof names)); *)
try
debug_print (lazy (CicPp.ppterm goal_proof));