diff options
| author | Maxime Dénès | 2016-09-30 12:58:03 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2016-09-30 12:58:03 +0200 |
| commit | a7a3e5b4d6df64b9bee42a86cd018c19ac6b01c0 (patch) | |
| tree | 938a412d43a2e14c42ac42cb197f1654f6f839f9 /ltac | |
| parent | 7543449792d417a92092b692986d62b622b78ffc (diff) | |
| parent | c4c7aa6d7b14a6d76c287b97d487abe055406577 (diff) | |
Merge remote-tracking branch 'github/pr/303' into v8.6
Was PR#303: LtacProf cutoff is for total percent, not time
Diffstat (limited to 'ltac')
| -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 a91ff98fb9..2514ededb0 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 () ++ |