aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--dev/doc/changes.md7
-rw-r--r--engine/termops.ml12
-rw-r--r--ide/coqide/protocol/xmlprotocol.ml4
-rw-r--r--kernel/univ.ml6
-rw-r--r--kernel/vmbytecodes.ml6
-rw-r--r--lib/explore.ml2
-rw-r--r--lib/pp.ml20
-rw-r--r--lib/pp.mli4
-rw-r--r--parsing/ppextend.ml4
-rw-r--r--parsing/ppextend.mli2
-rw-r--r--plugins/extraction/scheme.ml2
-rw-r--r--plugins/funind/gen_principle.ml6
-rw-r--r--plugins/ltac/pptactic.ml2
-rw-r--r--plugins/ltac/profile_ltac.ml4
-rw-r--r--pretyping/reductionops.ml4
-rw-r--r--printing/ppconstr.ml2
-rw-r--r--proofs/clenv.ml2
-rw-r--r--tactics/cbn.ml2
-rw-r--r--vernac/himsg.ml6
-rw-r--r--vernac/prettyp.ml2
20 files changed, 54 insertions, 45 deletions
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/xmlprotocol.ml b/ide/coqide/protocol/xmlprotocol.ml
index 56a934b8d4..9e861baac6 100644
--- a/ide/coqide/protocol/xmlprotocol.ml
+++ b/ide/coqide/protocol/xmlprotocol.ml
@@ -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))
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 6d8aa02dff..d910b102d8 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -250,7 +250,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
@@ -961,7 +961,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)
@@ -1076,7 +1076,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 =
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 10:26:07 +0000