Ltac_plugin.Profile_ltac
Ltac profiling primitives
val do_profile : string -> ('a * Tacexpr.ltac_call_kind) list -> ?count_call:bool -> 'b Proofview.tactic -> 'b Proofview.tactic
type treenode = {
name : CString.Map.key; |
total : float; |
local : float; |
ncalls : int; |
max_total : float; |
children : treenode CString.Map.t; |
}
val get_local_profiling_results : unit -> treenode
val feedback_results : treenode -> unit