diff options
Diffstat (limited to 'ltac/profile_ltac_tactics.ml4')
| -rw-r--r-- | ltac/profile_ltac_tactics.ml4 | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/ltac/profile_ltac_tactics.ml4 b/ltac/profile_ltac_tactics.ml4 index c092a0cb6..9083bda60 100644 --- a/ltac/profile_ltac_tactics.ml4 +++ b/ltac/profile_ltac_tactics.ml4 @@ -31,7 +31,8 @@ VERNAC COMMAND EXTEND ResetLtacProfiling CLASSIFIED AS SIDEFF END VERNAC COMMAND EXTEND ShowLtacProfile CLASSIFIED AS QUERY - [ "Show" "Ltac" "Profile" ] -> [ print_results() ] +| [ "Show" "Ltac" "Profile" ] -> [ print_results ~cutoff:0.0 ] +| [ "Show" "Ltac" "Profile" "CutOff" int(n) ] -> [ print_results ~cutoff:(float_of_int n) ] END VERNAC COMMAND EXTEND ShowLtacProfileTactic CLASSIFIED AS QUERY |