 +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 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)
++  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() =
++let header() = 
 +  msgnl(str" tactic                                    self  total   calls       max");
 +  msgnl(str"────────────────────────────────────────┴──────┴──────┴───────┴─────────┘")
 +

+  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

+++ 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
