1 files changed, 26 insertions, 5 deletions

diff --git a/plugins/ltac/profile_ltac.ml b/plugins/ltac/profile_ltac.ml
index 9ae8bfe65b..1615465281 100644
--- a/plugins/ltac/profile_ltac.ml
+++ b/plugins/ltac/profile_ltac.ml
@@ -289,7 +289,7 @@ let rec find_in_stack what acc = function
   | { name } as x :: rest when String.equal name what -> Some(acc, x, rest)
   | { name } as x :: rest -> find_in_stack what (x :: acc) rest
 
-let exit_tactic start_time c =
+let exit_tactic ~count_call start_time c =
   let diff = time () -. start_time in
   match Local.(!stack) with
   | [] | [_] ->
@@ -304,7 +304,7 @@ let exit_tactic start_time c =
     let node = { node with
       total = node.total +. diff;
       local = node.local +. diff;
-      ncalls = node.ncalls + 1;
+      ncalls = node.ncalls + (if count_call then 1 else 0);
       max_total = max node.max_total diff;
     } in
     (* updating the stack *)
@@ -341,7 +341,7 @@ let tclFINALLY tac (finally : unit Proofview.tactic) =
     (fun v -> finally <*> Proofview.tclUNIT v)
     (fun (exn, info) -> finally <*> Proofview.tclZERO ~info exn)
 
-let do_profile s call_trace tac =
+let do_profile s call_trace ?(count_call=true) tac =
   let open Proofview.Notations in
   Proofview.tclLIFT (Proofview.NonLogical.make (fun () ->
   if !is_profiling then
@@ -359,7 +359,7 @@ let do_profile s call_trace tac =
       tac
       (Proofview.tclLIFT (Proofview.NonLogical.make (fun () ->
         (match call_trace with
-        | (_, c) :: _ -> exit_tactic start_time c
+        | (_, c) :: _ -> exit_tactic ~count_call start_time c
         | [] -> ()))))
   | None -> tac
 
@@ -397,6 +397,27 @@ let reset_profile () =
   reset_profile_tmp ();
   data := SM.empty
 
+(* ****************************** Named timers ****************************** *)
+
+let timer_data = ref M.empty
+
+let timer_name = function
+  | Some v -> v
+  | None -> ""
+
+let restart_timer name =
+  timer_data := M.add (timer_name name) (System.get_time ()) !timer_data
+
+let get_timer name =
+  try M.find (timer_name name) !timer_data
+  with Not_found -> System.get_time ()
+
+let finish_timing ~prefix name =
+  let tend = System.get_time () in
+  let tstart = get_timer name in
+  Feedback.msg_info(str prefix ++ pr_opt str name ++ str " ran for " ++
+                    System.fmt_time_difference tstart tend)
+
 (* ******************** *)
 
 let print_results_filter ~cutoff ~filter =
@@ -408,7 +429,7 @@ let print_results_filter ~cutoff ~filter =
   let results =
     SM.fold (fun _ -> merge_roots ~disjoint:true) !data (empty_treenode root) in
   let results = merge_roots results Local.(CList.last !stack) in
-  Feedback.msg_notice (to_string ~cutoff ~filter results)
+  Feedback.msg_info (to_string ~cutoff ~filter results)
 ;;
 
 let print_results ~cutoff =