 +++ b/lib/pp.mli
 @@ -122,3 +122,6 @@ val msg_warn : string -> unit
  val msg_debug : std_ppcmds -> unit
-
+ 
  val string_of_ppcmds : std_ppcmds -> string
 +
 +val utf8_length : string -> int

+  print_table all_total indent false n.children
+
+and print_table all_total indent first_level table =
+  let ls = Hashtbl.fold
+	     (fun s n l -> if n.entry.total /. all_total < 0.02 then l else (s, n) :: l)
+      table [] in
+  match ls with
+  | [(s,n)]  when (not first_level) ->
+     print_node all_total indent (indent^"└") (s,n)
+  | _ ->
+     let ls = List.sort (fun (_, n1) (_, n2) -> compare n2.entry.total n1.entry.total) ls in
+     list_iter_is_last
+       (fun is_last ->
+	print_node
+	  all_total
+	  (indent^if first_level then "" else if is_last then "  " else " │")
+	  (indent^if first_level then "─" else if is_last then " └─" else " ├─")
+       )
+       ls
+

@@ -1962,7 +1964,7 @@ and eval_with_fail ist is_lazy goal tac =
     (match v with
     | VFun (trace,lfun,[],t) when not is_lazy ->
  let tac = eval_tactic {ist with lfun=lfun; trace=trace} t in
- VRTactic (catch_error trace tac { goal with sigma=sigma })
+ VRTactic (Profile_ltac.do_profile "eval_with_fail" trace (fun() -> catch_error trace tac { goal with sigma=sigma }))
     | a -> a)
   with
     | FailError (0,s) | Loc.Exc_located(_, FailError (0,s))
