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.
---
 engine/termops.ml | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

(limited to 'engine')

diff --git a/engine/termops.ml b/engine/termops.ml
index 0923ab6f4b..467b269e37 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -233,13 +233,13 @@ let pr_evar_universe_context ctx =
   if UState.is_empty ctx then mt ()
   else
     (str"UNIVERSES:"++brk(0,1)++
-       h 0 (Univ.pr_universe_context_set prl (UState.context_set ctx)) ++ fnl () ++
+       h (Univ.pr_universe_context_set prl (UState.context_set ctx)) ++ fnl () ++
      str"ALGEBRAIC UNIVERSES:"++brk(0,1)++
-     h 0 (Univ.LSet.pr prl (UState.algebraics ctx)) ++ fnl() ++
+     h (Univ.LSet.pr prl (UState.algebraics ctx)) ++ fnl() ++
      str"UNDEFINED UNIVERSES:"++brk(0,1)++
-     h 0 (UnivSubst.pr_universe_opt_subst (UState.subst ctx)) ++ fnl() ++
+     h (UnivSubst.pr_universe_opt_subst (UState.subst ctx)) ++ fnl() ++
      str "WEAK CONSTRAINTS:"++brk(0,1)++
-     h 0 (UState.pr_weak prl ctx) ++ fnl ())
+     h (UState.pr_weak prl ctx) ++ fnl ())
 
 let print_env_short env sigma =
   let print_constr = print_kconstr in
@@ -316,14 +316,14 @@ let pr_evar_list env sigma l =
     | Some ev' -> str " (aliased to " ++ Evar.print ev' ++ str ")"
   in
   let pr (ev, evi) =
-    h 0 (Evar.print ev ++
+    h (Evar.print ev ++
       str "==" ++ pr_evar_info env sigma evi ++
       pr_alias ev ++
       (if evi.evar_body == Evar_empty
        then str " {" ++ pr_existential_key sigma ev ++ str "}"
        else mt ()))
   in
-  h 0 (prlist_with_sep fnl pr l)
+  hv 0 (prlist_with_sep fnl pr l)
 
 let to_list d =
   let open Evd in
-- 
cgit v1.2.3