diff options
| author | Hugo Herbelin | 2020-10-05 22:21:04 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-10-08 23:47:14 +0200 |
| commit | db278921c54201a01543953cc0986fc0fb126615 (patch) | |
| tree | 70115f7e9365b34c4464affbb9a8cf71a925317c /plugins/ltac | |
| parent | e18ed350f7b5710c382ea1306e7b1e7e2fb0c9f8 (diff) | |
Dropping the misleading int argument of Pp.h.
An h-box inhibits the breaking semantics of any cut/spc/brk in the
enclosed box.
We tentatively replace its occurrence by an h or hv, assuming in
particular that if the indentation is not 0, an hv box was intended.
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 ++ |