diff options
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 50f9583f94..d2b7c70750 100644 --- a/ltac/profile_ltac.ml +++ b/ltac/profile_ltac.ml @@ -160,6 +160,7 @@ let rec print_node ~filter all_total indent prefix (s, e) = ++ padl 8 (string_of_int e.ncalls) ++ padl 10 (format_sec (e.max_total)) ) ++ + fnl () ++ print_table ~filter all_total indent false e.children and print_table ~filter all_total indent first_level table = @@ -179,7 +180,7 @@ and print_table ~filter all_total indent first_level table = let sep1 = if first_level then "─" else if is_last then " └─" else " ├─" in print_node ~filter all_total (indent ^ sep0) (indent ^ sep1) in - prlist_with_sep fnl (fun pr -> pr) (list_iter_is_last iter ls) + prlist (fun pr -> pr) (list_iter_is_last iter ls) let to_string ~filter node = let tree = node.children in @@ -224,7 +225,6 @@ let to_string ~filter node = header ++ print_table ~filter all_total "" true flat_tree ++ fnl () ++ - fnl () ++ header ++ print_table ~filter all_total "" true tree in |