- prerr_endline ("\n attempt: " ^
- NCicPp.ppterm ~metasenv ~subst ~context t1 ^ " ==?== " ^
- NCicPp.ppterm ~metasenv ~subst ~context c1 ^ " AND " ^
- NCicPp.ppterm ~metasenv ~subst ~context c2 ^ " ==?== " ^
- NCicPp.ppterm ~metasenv ~subst ~context t2);
+ prerr_endline ("\nProvo il candidato:\n" ^
+ String.concat "\n"
+ (List.map
+ (fun (a,b) ->
+ NCicPp.ppterm ~metasenv ~subst ~context a ^ " =?= " ^
+ NCicPp.ppterm ~metasenv ~subst ~context b) premises) ^
+ "\n-------------------------------------------\n"^
+ NCicPp.ppterm ~metasenv ~subst ~context c1 ^ " = " ^
+ NCicPp.ppterm ~metasenv ~subst ~context c2);