From db278921c54201a01543953cc0986fc0fb126615 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 5 Oct 2020 22:21:04 +0200
Subject: 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.
---
 plugins/ltac/pptactic.ml     | 2 +-
 plugins/ltac/profile_ltac.ml | 4 ++--
 2 files changed, 3 insertions(+), 3 deletions(-)

(limited to 'plugins/ltac')

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 ++
-- 
cgit v1.2.3