diff options
Diffstat (limited to 'ltac')
| -rw-r--r-- | ltac/profile_ltac.ml | 4 | ||||
| -rw-r--r-- | ltac/profile_ltac_tactics.ml4 | 2 |
2 files changed, 3 insertions, 3 deletions
diff --git a/ltac/profile_ltac.ml b/ltac/profile_ltac.ml index 102918e5e5..a91ff98fb9 100644 --- a/ltac/profile_ltac.ml +++ b/ltac/profile_ltac.ml @@ -401,11 +401,11 @@ let print_results ~cutoff = print_results_filter ~cutoff ~filter:(fun _ -> true) let print_results_tactic tactic = - print_results_filter ~cutoff:0.0 ~filter:(fun s -> + print_results_filter ~cutoff:!Flags.profile_ltac_cutoff ~filter:(fun s -> String.(equal tactic (sub (s ^ ".") 0 (min (1+length s) (length tactic))))) let do_print_results_at_close () = - if get_profiling () then print_results ~cutoff:0.0 + if get_profiling () then print_results ~cutoff:!Flags.profile_ltac_cutoff let _ = Declaremods.append_end_library_hook do_print_results_at_close diff --git a/ltac/profile_ltac_tactics.ml4 b/ltac/profile_ltac_tactics.ml4 index 9083bda60a..8cb76d81c5 100644 --- a/ltac/profile_ltac_tactics.ml4 +++ b/ltac/profile_ltac_tactics.ml4 @@ -31,7 +31,7 @@ VERNAC COMMAND EXTEND ResetLtacProfiling CLASSIFIED AS SIDEFF END VERNAC COMMAND EXTEND ShowLtacProfile CLASSIFIED AS QUERY -| [ "Show" "Ltac" "Profile" ] -> [ print_results ~cutoff:0.0 ] +| [ "Show" "Ltac" "Profile" ] -> [ print_results ~cutoff:!Flags.profile_ltac_cutoff ] | [ "Show" "Ltac" "Profile" "CutOff" int(n) ] -> [ print_results ~cutoff:(float_of_int n) ] END |