diff options
Diffstat (limited to 'ltac/profile_ltac.mli')
| -rw-r--r-- | ltac/profile_ltac.mli | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/ltac/profile_ltac.mli b/ltac/profile_ltac.mli index 8c4b47b8e..e5e2e4197 100644 --- a/ltac/profile_ltac.mli +++ b/ltac/profile_ltac.mli @@ -14,7 +14,8 @@ val do_profile : val set_profiling : bool -> unit -val print_results : unit -> unit +(* Cut off results < than specified cutoff *) +val print_results : cutoff:float -> unit val print_results_tactic : string -> unit |