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/funind/gen_principle.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'plugins/funind')

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