diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-09-29 18:28:24 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2016-09-29 18:57:52 -0400 |
| commit | c4c7aa6d7b14a6d76c287b97d487abe055406577 (patch) | |
| tree | e80e74a11f69139f8b480298e7a27a3cf905f427 /ltac/profile_ltac.ml | |
| parent | edb55a94fc5c0473e57f5a61c0c723194c2ff414 (diff) | |
LtacProf cutoff is for total percent, not time
Diffstat (limited to 'ltac/profile_ltac.ml')
| -rw-r--r-- | ltac/profile_ltac.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/ltac/profile_ltac.ml b/ltac/profile_ltac.ml index a91ff98fb..2514ededb 100644 --- a/ltac/profile_ltac.ml +++ b/ltac/profile_ltac.ml @@ -128,7 +128,7 @@ let to_ltacprof_results xml = | _ -> CErrors.anomaly Pp.(str "Malformed ltacprof XML") let feedback_results results = - Feedback.(feedback + Feedback.(feedback (Custom (Loc.dummy_loc, "ltacprof_results", of_ltacprof_results results))) (* ************** pretty printing ************************************* *) @@ -218,7 +218,7 @@ let to_string ~filter ?(cutoff=0.0) node = !global in warn_encountered_multi_success_backtracking (); - let filter s n = filter s && n >= cutoff in + let filter s n = filter s && (all_total <= 0.0 || n /. all_total >= cutoff /. 100.0) in let msg = h 0 (str "total time: " ++ padl 11 (format_sec (all_total))) ++ fnl () ++ |