Merge PR #13143: Drop misleading argument of Pp.h box

Reviewed-by: ejgallego
Reviewed-by: silene

23 files changed, 76 insertions, 52 deletions

diff --git a/dev/ci/user-overlays/13143-herbelin-master+drop-misleading-arg-hbox.sh b/dev/ci/user-overlays/13143-herbelin-master+drop-misleading-arg-hbox.sh
new file mode 100644
index 0000000000..1b3121781b
--- /dev/null
+++ b/dev/ci/user-overlays/13143-herbelin-master+drop-misleading-arg-hbox.sh
@@ -0,0 +1,9 @@
+if [ "$CI_PULL_REQUEST" = "13143" ] || [ "$CI_BRANCH" = "master+drop-misleading-arg-hbox" ]; then
+
+    aac_tactics_CI_REF=master+adapt-coq-pr13143-hbox-no-argument
+    aac_tactics_CI_GITURL=https://github.com/herbelin/aac-tactics
+
+    equations_CI_REF=master+adapt-coq-pr13143-hbox-no-argument
+    equations_CI_GITURL=https://github.com/herbelin/Coq-Equations
+
+fi
diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index 59c1623a2d..fb5d7cc244 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -10,6 +10,13 @@
   git hook removed. If desired, automatic formatting can be achieved by calling
   the `fmt` target of the dune build system.
 
+### Pp library
+
+- `Pp.h` does not take a `int` argument anymore (the argument was
+  not used). In general, where `h n` for `n` non zero was used, `hv n`
+  was instead intended. If cancelling the breaking role of cuts in the
+  box was intended, turn `h n c` into `h c`.
+
 ## Changes between Coq 8.11 and Coq 8.12
 
 ### Code formatting
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
diff --git a/ide/coqide/protocol/serialize.ml b/ide/coqide/protocol/serialize.ml
index bdbec5b30f..6a0a3d7f5d 100644
--- a/ide/coqide/protocol/serialize.ml
+++ b/ide/coqide/protocol/serialize.ml
@@ -35,6 +35,11 @@ let singleton = function
   | l -> raise (Marshal_error
       ("singleton",PCData ("list of length " ^ string_of_int (List.length l))))
 
+let empty = function
+  | [] -> ()
+  | l -> raise (Marshal_error
+      ("empty",PCData ("list of length " ^ string_of_int (List.length l))))
+
 let raw_string = function
   | [] -> ""
   | [PCData s] -> s
diff --git a/ide/coqide/protocol/serialize.mli b/ide/coqide/protocol/serialize.mli
index 5d88defe55..9d09b81d1e 100644
--- a/ide/coqide/protocol/serialize.mli
+++ b/ide/coqide/protocol/serialize.mli
@@ -16,6 +16,7 @@ val massoc: string -> (string * string) list -> string
 val constructor: string -> string -> xml list -> xml
 val do_match: string -> (string -> xml list -> 'b) -> xml -> 'b
 val singleton: 'a list -> 'a
+val empty: 'a list -> unit
 val raw_string: xml list -> string
 val of_unit: unit -> xml
 val to_unit: xml -> unit
diff --git a/ide/coqide/protocol/xmlprotocol.ml b/ide/coqide/protocol/xmlprotocol.ml
index 6cb0cec008..9e861baac6 100644
--- a/ide/coqide/protocol/xmlprotocol.ml
+++ b/ide/coqide/protocol/xmlprotocol.ml
@@ -43,7 +43,7 @@ let to_search_cst = do_match "search_cst" (fun s args -> match s with
   | "type_pattern" -> Type_Pattern (to_string (singleton args))
   | "subtype_pattern" -> SubType_Pattern (to_string (singleton args))
   | "in_module" -> In_Module (to_list to_string (singleton args))
-  | "include_blacklist" -> Include_Blacklist
+  | "include_blacklist" -> empty args; Include_Blacklist
   | x -> raise (Marshal_error("search",PCData x)))
 
 let of_coq_object f ans =
@@ -103,14 +103,14 @@ let to_routeid = function
 let of_routeid i = Element ("route_id",["val",string_of_int i],[])
 
 let of_box (ppb : Pp.block_type) = let open Pp in match ppb with
-  | Pp_hbox   i -> constructor "ppbox" "hbox"   [of_int i]
+  | Pp_hbox     -> constructor "ppbox" "hbox"   []
   | Pp_vbox   i -> constructor "ppbox" "vbox"   [of_int i]
   | Pp_hvbox  i -> constructor "ppbox" "hvbox"  [of_int i]
   | Pp_hovbox i -> constructor "ppbox" "hovbox" [of_int i]
 
 let to_box = let open Pp in
   do_match "ppbox" (fun s args -> match s with
-      | "hbox"   -> Pp_hbox   (to_int (singleton args))
+      | "hbox"   -> empty args; Pp_hbox
       | "vbox"   -> Pp_vbox   (to_int (singleton args))
       | "hvbox"  -> Pp_hvbox  (to_int (singleton args))
       | "hovbox" -> Pp_hovbox (to_int (singleton args))
@@ -132,7 +132,7 @@ let rec of_pp (pp : Pp.t) = let open Pp in match Pp.repr pp with
 let rec to_pp xpp = let open Pp in
   Pp.unrepr @@
   do_match "ppdoc" (fun s args -> match s with
-    | "empty"     -> Ppcmd_empty
+    | "empty"     -> empty args; Ppcmd_empty
     | "string"    -> Ppcmd_string (to_string (singleton args))
     | "glue"      -> Ppcmd_glue (to_list to_pp (singleton args))
     | "box"       -> let (bt,s) = to_pair to_box to_pp (singleton args) in
@@ -858,11 +858,11 @@ let of_message_level = function
   | Error -> Serialize.constructor "message_level" "error" []
 let to_message_level =
   Serialize.do_match "message_level" (fun s args -> match s with
-  | "debug" -> Debug
-  | "info" -> Info
-  | "notice" -> Notice
-  | "warning" -> Warning
-  | "error" -> Error
+  | "debug" -> empty args; Debug
+  | "info" -> empty args; Info
+  | "notice" -> empty args; Notice
+  | "warning" -> empty args; Warning
+  | "error" -> empty args; Error
   | x -> raise Serialize.(Marshal_error("error level",PCData x)))
 
 let of_message lvl loc msg =
diff --git a/kernel/univ.ml b/kernel/univ.ml
index d2fb04bc38..a2fd14025e 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -244,7 +244,7 @@ module LMap = struct
       ext empty
 
   let pr f m =
-    h 0 (prlist_with_sep fnl (fun (u, v) ->
+    h (prlist_with_sep fnl (fun (u, v) ->
       Level.pr u ++ f v) (bindings m))
 end
 
@@ -943,7 +943,7 @@ struct
 
   let pr prl ?variance (univs, cst as ctx) =
     if is_empty ctx then mt() else
-      h 0 (Instance.pr prl ?variance univs ++ str " |= ") ++ h 0 (v 0 (Constraint.pr prl cst))
+      h (Instance.pr prl ?variance univs ++ str " |= ") ++ h (v 0 (Constraint.pr prl cst))
 
   let hcons (univs, cst) =
     (Instance.hcons univs, hcons_constraints cst)
@@ -1058,7 +1058,7 @@ struct
 
   let pr prl (univs, cst as ctx) =
     if is_empty ctx then mt() else
-      h 0 (LSet.pr prl univs ++ str " |= ") ++ h 0 (v 0 (Constraint.pr prl cst))
+      h (LSet.pr prl univs ++ str " |= ") ++ h (v 0 (Constraint.pr prl cst))
 
   let constraints (_univs, cst) = cst
   let levels (univs, _cst) = univs
diff --git a/kernel/vmbytecodes.ml b/kernel/vmbytecodes.ml
index 74405a0105..c156a21c86 100644
--- a/kernel/vmbytecodes.ml
+++ b/kernel/vmbytecodes.ml
@@ -106,14 +106,14 @@ let rec pp_instr i =
   | Kclosure(lbl, n) ->
       str "closure " ++ pp_lbl lbl ++ str ", " ++ int n
   | Kclosurerec(fv,init,lblt,lblb) ->
-      h 1 (str "closurerec " ++
+      hv 1 (str "closurerec " ++
              int fv ++ str ", " ++ int init ++
              str " types = " ++
              prlist_with_sep spc pp_lbl (Array.to_list lblt) ++
              str " bodies = " ++
              prlist_with_sep spc pp_lbl (Array.to_list lblb))
   | Kclosurecofix (fv,init,lblt,lblb) ->
-      h 1 (str "closurecofix " ++
+      hv 1 (str "closurecofix " ++
              int fv ++ str ", " ++ int init ++
              str " types = " ++
              prlist_with_sep spc pp_lbl (Array.to_list lblt) ++
@@ -129,7 +129,7 @@ let rec pp_instr i =
       str "makeswitchblock " ++ pp_lbl lblt ++ str ", " ++
         pp_lbl lbls ++ str ", " ++ int sz
   | Kswitch(lblc,lblb) ->
-      h 1 (str "switch " ++
+      hv 1 (str "switch " ++
              prlist_with_sep spc pp_lbl (Array.to_list lblc) ++
              str " | " ++
              prlist_with_sep spc pp_lbl (Array.to_list lblb))
diff --git a/lib/explore.ml b/lib/explore.ml
index b3ffef6ac2..139de488e2 100644
--- a/lib/explore.ml
+++ b/lib/explore.ml
@@ -29,7 +29,7 @@ module Make = functor(S : SearchProblem) -> struct
       | [i] -> int i
       | i :: l -> pp_rec l ++ str "." ++ int i
     in
-    Feedback.msg_debug (h 0 (pp_rec p) ++ pp)
+    Feedback.msg_debug (h (pp_rec p) ++ pp)
 
   (*s Depth first search. *)
 
diff --git a/lib/pp.ml b/lib/pp.ml
index 78c5186449..a9994ac6fd 100644
--- a/lib/pp.ml
+++ b/lib/pp.ml
@@ -22,7 +22,7 @@
 type pp_tag = string
 
 type block_type =
-  | Pp_hbox   of int
+  | Pp_hbox
   | Pp_vbox   of int
   | Pp_hvbox  of int
   | Pp_hovbox of int
@@ -131,7 +131,7 @@ let strbrk s =
 let ismt = function | Ppcmd_empty -> true | _ -> false
 
 (* boxing commands *)
-let h   n s = Ppcmd_box(Pp_hbox n,s)
+let h     s = Ppcmd_box(Pp_hbox,s)
 let v   n s = Ppcmd_box(Pp_vbox n,s)
 let hv  n s = Ppcmd_box(Pp_hvbox n,s)
 let hov n s = Ppcmd_box(Pp_hovbox n,s)
@@ -151,7 +151,7 @@ let escape_string s =
 
 let qstring s = str "\"" ++ str (escape_string s) ++ str "\""
 let qs = qstring
-let quote s = h 0 (str "\"" ++ s ++ str "\"")
+let quote s = h (str "\"" ++ s ++ str "\"")
 
 let rec pr_com ft s =
   let (s1,os) =
@@ -181,7 +181,7 @@ let split_tag tag =
 (* pretty printing functions *)
 let pp_with ft pp =
   let cpp_open_box = function
-    | Pp_hbox n   -> Format.pp_open_hbox ft ()
+    | Pp_hbox     -> Format.pp_open_hbox ft ()
     | Pp_vbox n   -> Format.pp_open_vbox ft n
     | Pp_hvbox n  -> Format.pp_open_hvbox ft n
     | Pp_hovbox n -> Format.pp_open_hovbox ft n
@@ -309,12 +309,14 @@ let db_print_pp fmt pp =
   let block_type fmt btype =
     let (bt, v) =
       match btype with
-      | Pp_hbox v -> ("Pp_hbox", v)
-      | Pp_vbox v -> ("Pp_vbox", v)
-      | Pp_hvbox v -> ("Pp_hvbox", v)
-      | Pp_hovbox v -> ("Pp_hovbox", v)
+      | Pp_hbox -> ("Pp_hbox", None)
+      | Pp_vbox v -> ("Pp_vbox", Some v)
+      | Pp_hvbox v -> ("Pp_hvbox", Some v)
+      | Pp_hovbox v -> ("Pp_hovbox", Some v)
     in
-    fprintf fmt "%s %d" bt v
+    match v with
+    | None -> fprintf fmt "%s" bt
+    | Some v -> fprintf fmt "%s %d" bt v
   in
   let rec db_print_pp_r indent pp =
     let ind () = fprintf fmt "%s" (String.make (2 * indent) ' ') in
diff --git a/lib/pp.mli b/lib/pp.mli
index b265537728..12f1ba9bb2 100644
--- a/lib/pp.mli
+++ b/lib/pp.mli
@@ -43,7 +43,7 @@ type pp_tag = string
 type t
 
 type block_type =
-  | Pp_hbox   of int
+  | Pp_hbox
   | Pp_vbox   of int
   | Pp_hvbox  of int
   | Pp_hovbox of int
@@ -99,7 +99,7 @@ val strbrk : string -> t
 
 (** {6 Boxing commands} *)
 
-val h : int -> t -> t
+val h : t -> t
 val v : int -> t -> t
 val hv : int -> t -> t
 val hov : int -> t -> t
diff --git a/parsing/ppextend.ml b/parsing/ppextend.ml
index fe6e8360c1..aab385a707 100644
--- a/parsing/ppextend.ml
+++ b/parsing/ppextend.ml
@@ -17,7 +17,7 @@ open Constrexpr
 (*s Pretty-print. *)
 
 type ppbox =
-  | PpHB of int
+  | PpHB
   | PpHOVB of int
   | PpHVB of int
   | PpVB of int
@@ -27,7 +27,7 @@ type ppcut =
   | PpFnl
 
 let ppcmd_of_box = function
-  | PpHB n -> h n
+  | PpHB -> h
   | PpHOVB n -> hov n
   | PpHVB n -> hv n
   | PpVB n -> v n
diff --git a/parsing/ppextend.mli b/parsing/ppextend.mli
index ee8180c7aa..56a3fc8e3c 100644
--- a/parsing/ppextend.mli
+++ b/parsing/ppextend.mli
@@ -13,7 +13,7 @@ open Constrexpr
 (** {6 Pretty-print. } *)
 
 type ppbox =
-  | PpHB of int
+  | PpHB
   | PpHOVB of int
   | PpHVB of int
   | PpVB of int
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 ++
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index aeb18ec322..08a6db5639 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -445,7 +445,7 @@ type state_reduction_function =
 let pr_state env sigma (tm,sk) =
   let open Pp in
   let pr c = Termops.Internal.print_constr_env env sigma c in
-  h 0 (pr tm ++ str "|" ++ cut () ++ Stack.pr pr sk)
+  h (pr tm ++ str "|" ++ cut () ++ Stack.pr pr sk)
 
 (*************************************)
 (*** Reduction Functions Operators ***)
@@ -705,7 +705,7 @@ let rec whd_state_gen flags env sigma =
         let open Pp in
         let pr c = Termops.Internal.print_constr_env env sigma c in
         Feedback.msg_debug
-             (h 0 (str "<<" ++ pr x ++
+               (h (str "<<" ++ pr x ++
                    str "|" ++ cut () ++ Stack.pr pr stack ++
                    str ">>"))
     in
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index af105f4d63..267f5e0b5f 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -467,7 +467,7 @@ let tag_var = tag Tag.variable
   let pr_record_body_gen pr l =
     spc () ++
     prlist_with_sep pr_semicolon
-      (fun (id, c) -> h 1 (pr_reference id ++ spc () ++ str":=" ++ pr ltop c)) l
+      (fun (id, c) -> pr_reference id ++ str" :=" ++ pr ltop c) l
 
   let pr_forall n = keyword "forall" ++ pr_com_at n ++ spc ()
 
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)
diff --git a/tactics/cbn.ml b/tactics/cbn.ml
index 8f0966a486..0b13f4763a 100644
--- a/tactics/cbn.ml
+++ b/tactics/cbn.ml
@@ -543,7 +543,7 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma =
         let open Pp in
         let pr c = Termops.Internal.print_constr_env env sigma c in
         Feedback.msg_debug
-             (h 0 (str "<<" ++ pr x ++
+               (h (str "<<" ++ pr x ++
                    str "|" ++ cut () ++ Cst_stack.pr env sigma cst_l ++
                    str "|" ++ cut () ++ Stack.pr pr stack ++
                    str ">>"))
diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index c16eaac516..a9de01bfd0 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -831,7 +831,7 @@ let pr_constraints printenv env sigma evars cstrs =
         (fun (ev, evi) -> fnl () ++ pr_existential_key sigma ev ++
             str " : " ++ pr_leconstr_env env' sigma evi.evar_concl ++ fnl ()) l
       in
-      h 0 (pe ++ evs ++ pr_evar_constraints sigma cstrs)
+      h (pe ++ evs ++ pr_evar_constraints sigma cstrs)
     else
       let filter evk _ = Evar.Map.mem evk evars in
       pr_evar_map_filter ~with_univs:false filter env sigma
@@ -973,8 +973,8 @@ let explain_not_match_error = function
         (UContext.instance uctx)
         (UContext.constraints uctx)
     in
-    str "incompatible polymorphic binders: got" ++ spc () ++ h 0 (pr_auctx got) ++ spc() ++
-    str "but expected" ++ spc() ++ h 0 (pr_auctx expect) ++
+    str "incompatible polymorphic binders: got" ++ spc () ++ h (pr_auctx got) ++ spc() ++
+    str "but expected" ++ spc() ++ h (pr_auctx expect) ++
     (if not (Int.equal (AUContext.size got) (AUContext.size expect)) then mt() else
        fnl() ++ str "(incompatible constraints)")
   | IncompatibleVariance ->
diff --git a/vernac/prettyp.ml b/vernac/prettyp.ml
index 8b00484b4a..06f7c32cdc 100644
--- a/vernac/prettyp.ml
+++ b/vernac/prettyp.ml
@@ -216,7 +216,7 @@ let print_polymorphism ref =
       (if poly then str "universe polymorphic"
        else if template_poly then
          str "template universe polymorphic "
-         ++ h 0 (pr_template_variables template_variables)
+         ++ h (pr_template_variables template_variables)
        else str "not universe polymorphic") ]
 
 let print_type_in_type ref =