From 9043add656177eeac1491a73d2f3ab92bec0013c Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Sat, 29 Dec 2018 14:31:27 -0500 Subject: Imported Upstream version 8.8.2 --- ltac/profile_ltac.mli | 48 ------------------------------------------------ 1 file changed, 48 deletions(-) delete mode 100644 ltac/profile_ltac.mli (limited to 'ltac/profile_ltac.mli') diff --git a/ltac/profile_ltac.mli b/ltac/profile_ltac.mli deleted file mode 100644 index e5e2e419..00000000 --- a/ltac/profile_ltac.mli +++ /dev/null @@ -1,48 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* ('a * Tacexpr.ltac_call_kind) list -> - 'b Proofview.tactic -> 'b Proofview.tactic - -val set_profiling : bool -> unit - -(* Cut off results < than specified cutoff *) -val print_results : cutoff:float -> unit - -val print_results_tactic : string -> unit - -val reset_profile : unit -> unit - -val do_print_results_at_close : unit -> unit - -(* The collected statistics for a tactic. The timing data is collected over all - * instances of a given tactic from its parent. E.g. if tactic 'aaa' calls - * 'foo' twice, then 'aaa' will contain just one entry for 'foo' with the - * statistics of the two invocations combined, and also combined over all - * invocations of 'aaa'. - * total: time spent running this tactic and its subtactics (seconds) - * local: time spent running this tactic, minus its subtactics (seconds) - * ncalls: the number of invocations of this tactic that have been made - * max_total: the greatest running time of a single invocation (seconds) - *) -type treenode = { - name : CString.Map.key; - total : float; - local : float; - ncalls : int; - max_total : float; - children : treenode CString.Map.t -} - -(* Returns the profiling results known by the current process *) -val get_local_profiling_results : unit -> treenode -val feedback_results : treenode -> unit - -- cgit v1.2.3