From c4c7aa6d7b14a6d76c287b97d487abe055406577 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Thu, 29 Sep 2016 18:28:24 -0400
Subject: LtacProf cutoff is for total percent, not time

---
 ltac/profile_ltac.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'ltac')

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 () ++
-- 
cgit v1.2.3