-(*
- prerr_endline "Hints:";
- List.iter
- (fun (metasenv, (t1, t2), premises) ->
- prerr_endline
- ("\t" ^ String.concat "; "
- (List.map (fun (a,b) ->
- NCicPp.ppterm ~margin:max_int ~metasenv ~subst ~context a ^
- " =?= "^
- NCicPp.ppterm ~margin:max_int ~metasenv ~subst ~context b)
- premises) ^
- " ==> "^
- NCicPp.ppterm ~margin:max_int ~metasenv ~subst ~context t1 ^
- " = "^NCicPp.ppterm ~margin:max_int ~metasenv ~subst ~context t2))
- rc;
-*)
+
+ debug(lazy ("Hints:"^
+ String.concat "\n" (List.map
+ (fun (metasenv, (t1, t2), premises) ->
+ ("\t" ^ String.concat "; "
+ (List.map (fun (a,b) ->
+ NCicPp.ppterm ~margin:max_int ~metasenv ~subst ~context a ^
+ " =?= "^
+ NCicPp.ppterm ~margin:max_int ~metasenv ~subst ~context b)
+ premises) ^
+ " ==> "^
+ NCicPp.ppterm ~margin:max_int ~metasenv ~subst ~context t1 ^
+ " = "^NCicPp.ppterm ~margin:max_int ~metasenv ~subst ~context t2))
+ rc)));
+