 --- a/tactics/tacinterp.ml
 +++ b/tactics/tacinterp.ml
 @@ -277,7 +277,7 @@ let lookup_genarg_subst  id = let (_,_,f) = lookup_genarg id in f
-
+ 
  let push_trace (loc,ck) = function
    | (n,loc',ck')::trl when ck=ck' -> (n+1,loc,ck)::trl
 -  | trl -> (1,loc,ck)::trl
 +  | trl -> Profile_ltac.entered_call(); (1,loc,ck)::trl
-
+ 
  let propagate_trace ist loc id = function
    | VFun (_,lfun,it,b) ->
 @@ -1793,7 +1793,9 @@ and eval_tactic ist = function
- 	  catch_error (push_trace(dloc,call)ist.trace)
- 	    (interp_atomic ist gl) t	in
- 	(* catch error in the evaluation *)
--	catch_error (push_trace(loc,call)ist.trace) tac gl
-+	let trace = push_trace(loc,call)ist.trace in
-+	Profile_ltac.do_profile "eval_tactic:2" trace (fun()->
-+	  catch_error trace tac gl)
+    catch_error (push_trace(dloc,call)ist.trace)
+      (interp_atomic ist gl) t  in
+  (* catch error in the evaluation *)
+- catch_error (push_trace(loc,call)ist.trace) tac gl
++ let trace = push_trace(loc,call)ist.trace in
++ Profile_ltac.do_profile "eval_tactic:2" trace (fun()->
++   catch_error trace tac gl)
    | TacFun _ | TacLetIn _ -> assert false
    | TacMatchGoal _ | TacMatch _ -> assert false
    | TacId s -> fun gl ->

+  msgnl(str"");
+  header();
+  print_table tactic_total "" true table_tactic
+
+let reset_profile() = stack := [{entry=empty_entry(); children=Hashtbl.create 20}]
diff --git a/tactics/profile_ltac.mli b/tactics/profile_ltac.mli
new file mode 100644

+let format_ratio x = (Printf.sprintf "%.1f%%" (100. *. x))
+let padl n s = ws (max 0 (n - utf8_length s)) ++ str s
+let padr n s = str s ++ ws (max 0 (n - utf8_length s))
+let padr_with c n s = 
+  let ulength = utf8_length s in
+  let length = String.length s in
+  str (utf8_sub s 0 n) ++ str(String.make (max 0 (n - ulength)) c)  
+
+let rec list_iter_is_last f = function
+  | []      -> ()
+  | [x]     -> f true x
+  | x :: xs -> f false x; list_iter_is_last f xs
+
+let header() = 
+  msgnl(str" tactic                                    self  total   calls       max");
+  msgnl(str"────────────────────────────────────────┴──────┴──────┴───────┴─────────┘")
+
