Merge branch 'v8.6'

4 files changed, 17 insertions, 20 deletions

diff --git a/ltac/g_class.ml4 b/ltac/g_class.ml4
index d551b7315a..f8654d3903 100644
--- a/ltac/g_class.ml4
+++ b/ltac/g_class.ml4
@@ -44,18 +44,10 @@ ARGUMENT EXTEND debug TYPED AS bool PRINTED BY pr_debug
 | [ ] -> [ false ]
 END
 
-let pr_depth _prc _prlc _prt = function
-    Some i -> Pp.int i
-  | None -> Pp.mt()
-
-ARGUMENT EXTEND depth TYPED AS int option PRINTED BY pr_depth
-  | [ int_or_var_opt(v) ] -> [ match v with Some (ArgArg i) -> Some i | _ -> None ]
-END
-
 (* true = All transparent, false = Opaque if possible *)
 
 VERNAC COMMAND EXTEND Typeclasses_Settings CLASSIFIED AS SIDEFF
- | [ "Typeclasses" "eauto" ":=" debug(d) depth(depth) ] -> [
+ | [ "Typeclasses" "eauto" ":=" debug(d) int_opt(depth) ] -> [
      set_typeclasses_debug d;
      set_typeclasses_depth depth
    ]
@@ -63,9 +55,9 @@ END
 
 (** Compatibility: typeclasses eauto has 8.5 and 8.6 modes *)
 TACTIC EXTEND typeclasses_eauto
- | [ "typeclasses" "eauto" depth(d) "with" ne_preident_list(l) ] ->
+ | [ "typeclasses" "eauto" int_or_var_opt(d) "with" ne_preident_list(l) ] ->
     [ typeclasses_eauto d l ]
- | [ "typeclasses" "eauto" depth(d) ] -> [
+ | [ "typeclasses" "eauto" int_or_var_opt(d) ] -> [
      typeclasses_eauto ~only_classes:true ~depth:d [Hints.typeclasses_db] ]
 END
 
diff --git a/ltac/profile_ltac.ml b/ltac/profile_ltac.ml
index fe591c7756..102918e5e5 100644
--- a/ltac/profile_ltac.ml
+++ b/ltac/profile_ltac.ml
@@ -166,7 +166,7 @@ let rec print_node ~filter all_total indent prefix (s, e) =
 and print_table ~filter all_total indent first_level table =
   let fold _ n l =
     let s, total = n.name, n.total in
-    if filter s then (s, n) :: l else l in
+    if filter s total then (s, n) :: l else l in
   let ls = M.fold fold table [] in
   match ls with
   | [s, n] when not first_level ->
@@ -182,7 +182,7 @@ and print_table ~filter all_total indent first_level table =
     in
     prlist (fun pr -> pr) (list_iter_is_last iter ls)
 
-let to_string ~filter node =
+let to_string ~filter ?(cutoff=0.0) node =
   let tree = node.children in
   let all_total = M.fold (fun _ { total } a -> total +. a) node.children 0.0 in
   let flat_tree =
@@ -218,6 +218,7 @@ let to_string ~filter node =
     !global
   in
   warn_encountered_multi_success_backtracking ();
+  let filter s n = filter s && n >= cutoff in
   let msg =
     h 0 (str "total time: " ++ padl 11 (format_sec (all_total))) ++
     fnl () ++
@@ -387,22 +388,24 @@ let reset_profile () =
 
 (* ******************** *)
 
-let print_results_filter ~filter =
+let print_results_filter ~cutoff ~filter =
   let valid id _ = Stm.state_of_id id <> `Expired in
   data := SM.filter valid !data;
   let results =
     SM.fold (fun _ -> merge_roots ~disjoint:true) !data (empty_treenode root) in
   let results = merge_roots results Local.(CList.last !stack) in
-  Feedback.msg_notice (to_string ~filter results)
+  Feedback.msg_notice (to_string ~cutoff ~filter results)
 ;;
 
-let print_results () = print_results_filter ~filter:(fun _ -> true)
+let print_results ~cutoff =
+  print_results_filter ~cutoff ~filter:(fun _ -> true)
 
 let print_results_tactic tactic =
-  print_results_filter ~filter:(fun s ->
+  print_results_filter ~cutoff:0.0 ~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 ()
+let do_print_results_at_close () =
+  if get_profiling () then print_results ~cutoff:0.0
 
 let _ = Declaremods.append_end_library_hook do_print_results_at_close
 
diff --git a/ltac/profile_ltac.mli b/ltac/profile_ltac.mli
index 8c4b47b8e4..e5e2e41975 100644
--- a/ltac/profile_ltac.mli
+++ b/ltac/profile_ltac.mli
@@ -14,7 +14,8 @@ val do_profile :
 
 val set_profiling : bool -> unit
 
-val print_results : unit -> unit
+(* Cut off results < than specified cutoff *)
+val print_results : cutoff:float -> unit
 
 val print_results_tactic : string -> unit
 
diff --git a/ltac/profile_ltac_tactics.ml4 b/ltac/profile_ltac_tactics.ml4
index c092a0cb61..9083bda60a 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