diff options
| author | coqbot-app[bot] | 2020-10-09 14:43:02 +0000 |
|---|---|---|
| committer | GitHub | 2020-10-09 14:43:02 +0000 |
| commit | ac7c197c3b8a9b66956f35e364221938f91e2a23 (patch) | |
| tree | dac9632d48449cfe77977e209803ebb9d19b9805 /plugins/ltac | |
| parent | cc3ef68a475140bf7d3ca7a2fd3bc593508eb42c (diff) | |
| parent | f7fabd34526135daccce2630670905fc39e0c3db (diff) | |
Merge PR #13143: Drop misleading argument of Pp.h box
Reviewed-by: ejgallego
Reviewed-by: silene
Diffstat (limited to 'plugins/ltac')
| -rw-r--r-- | plugins/ltac/pptactic.ml | 2 | ||||
| -rw-r--r-- | plugins/ltac/profile_ltac.ml | 4 |
2 files changed, 3 insertions, 3 deletions
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index 85bb901046..cbb53497d3 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -179,7 +179,7 @@ let string_of_genarg_arg (ArgumentType arg) = | ConstrTypeOf c -> hov 1 (keyword "type of" ++ spc() ++ prc env sigma c) | ConstrTerm c when test c -> - h 0 (str "(" ++ prc env sigma c ++ str ")") + h (str "(" ++ prc env sigma c ++ str ")") | ConstrTerm c -> prc env sigma c diff --git a/plugins/ltac/profile_ltac.ml b/plugins/ltac/profile_ltac.ml index 0dbf16a821..9c15d24dd3 100644 --- a/plugins/ltac/profile_ltac.ml +++ b/plugins/ltac/profile_ltac.ml @@ -146,7 +146,7 @@ let header = fnl () let rec print_node ~filter all_total indent prefix (s, e) = - h 0 ( + h ( padr_with '-' 40 (prefix ^ s ^ " ") ++ padl 7 (format_ratio (e.local /. all_total)) ++ padl 7 (format_ratio (e.total /. all_total)) @@ -212,7 +212,7 @@ let to_string ~filter ?(cutoff=0.0) node = 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))) ++ + h (str "total time: " ++ padl 11 (format_sec (all_total))) ++ fnl () ++ fnl () ++ header ++ |