diff options
Diffstat (limited to 'plugins/ltac/profile_ltac.mli')
| -rw-r--r-- | plugins/ltac/profile_ltac.mli | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/plugins/ltac/profile_ltac.mli b/plugins/ltac/profile_ltac.mli index 52827cb36..07990c750 100644 --- a/plugins/ltac/profile_ltac.mli +++ b/plugins/ltac/profile_ltac.mli @@ -22,6 +22,10 @@ val print_results_tactic : string -> unit val reset_profile : unit -> unit +val restart_timer : string option -> unit + +val finish_timing : prefix:string -> string option -> unit + val do_print_results_at_close : unit -> unit (* The collected statistics for a tactic. The timing data is collected over all @@ -46,4 +50,3 @@ type treenode = { (* Returns the profiling results known by the current process *) val get_local_profiling_results : unit -> treenode val feedback_results : treenode -> unit - |