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 | |
| 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')
| -rw-r--r-- | plugins/extraction/scheme.ml | 2 | ||||
| -rw-r--r-- | plugins/funind/gen_principle.ml | 6 | ||||
| -rw-r--r-- | plugins/ltac/pptactic.ml | 2 | ||||
| -rw-r--r-- | plugins/ltac/profile_ltac.ml | 4 |
4 files changed, 7 insertions, 7 deletions
diff --git a/plugins/extraction/scheme.ml b/plugins/extraction/scheme.ml index ee50476b10..f671860bd5 100644 --- a/plugins/extraction/scheme.ml +++ b/plugins/extraction/scheme.ml @@ -28,7 +28,7 @@ let keywords = "error"; "delay"; "force"; "_"; "__"] Id.Set.empty -let pp_comment s = str";; "++h 0 s++fnl () +let pp_comment s = str ";; " ++ h s ++ fnl () let pp_header_comment = function | None -> mt () diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml index 1ea803f561..012fcee486 100644 --- a/plugins/funind/gen_principle.ml +++ b/plugins/funind/gen_principle.ml @@ -1860,13 +1860,13 @@ let do_generate_principle_aux pconstants on_error register_built let warn_cannot_define_graph = CWarnings.create ~name:"funind-cannot-define-graph" ~category:"funind" (fun (names, error) -> - Pp.(strbrk "Cannot define graph(s) for " ++ h 1 names ++ error)) + Pp.(strbrk "Cannot define graph(s) for " ++ hv 1 names ++ error)) let warn_cannot_define_principle = CWarnings.create ~name:"funind-cannot-define-principle" ~category:"funind" (fun (names, error) -> Pp.( - strbrk "Cannot define induction principle(s) for " ++ h 1 names ++ error)) + strbrk "Cannot define induction principle(s) for " ++ hv 1 names ++ error)) let warning_error names e = let e_explain e = @@ -1898,7 +1898,7 @@ let error_error names e = CErrors.user_err Pp.( str "Cannot define graph(s) for " - ++ h 1 + ++ hv 1 (prlist_with_sep (fun _ -> str "," ++ spc ()) Ppconstr.pr_id names) ++ e_explain e) | _ -> raise e 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 ++ |