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