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.
---
 proofs/clenv.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'proofs')

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 31bc698830..387f0f6f5f 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -720,7 +720,7 @@ let make_clenv_binding env sigma = make_clenv_binding_gen false None env sigma
 (* Pretty-print *)
 
 let pr_clenv clenv =
-  h 0
+  h
     (str"TEMPL: " ++ Termops.Internal.print_constr_env clenv.env clenv.evd clenv.templval.rebus ++
      str" : " ++ Termops.Internal.print_constr_env clenv.env clenv.evd clenv.templtyp.rebus ++ fnl () ++
      pr_evar_map (Some 2) clenv.env clenv.evd)
-- 
cgit v1.2.3