aboutsummaryrefslogtreecommitdiffhomepage
path: root/ltacprof/profile_ltac.mli
blob: dd750517e3ea99394e29efe935b48540038bbc7f (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
val do_profile : string -> ('a * Tacexpr.ltac_call_kind) list -> 'b Proofview.tactic -> 'b Proofview.tactic

val set_profiling : bool -> unit

val set_display_profile_at_close : bool -> unit

val entered_call : unit -> unit

val print_results : unit -> unit

val print_results_tactic : string -> unit

val reset_profile : unit -> unit

val do_print_results_at_close : unit -> unit