Message

Ltac2.Message

val print : message -> unit

print msg writes the message on the output stream.

val empty : message

empty is the empty message.

val of_string : string -> message

of_string s prints a string.

val to_string : message -> string

to_string s converts a message to a string.

val of_int : int -> message

of_int n prints an integer.

val of_ident : ident -> message

of_ident id prints an identifier.

val of_constr : Environ.env -> Evd.evar_map -> constr -> message

of_constr env sigma t prints t at level 8 (surrounding with parentheses to print syntax above that level such as applications).

val of_lconstr : Environ.env -> Evd.evar_map -> constr -> message

of_lconstr env sigma t prints t at level 200 (no surrounding parentheses).

val of_preterm : Environ.env -> Evd.evar_map -> preterm -> message

of_preterm env sigma t prints t at level 8 (surrounding with parentheses to print syntax above that level such as applications).

val of_lpreterm : Environ.env -> Evd.evar_map -> preterm -> message

of_lpreterm env sigma t prints t at level 200 (no surrounding parentheses).

val of_exninfo : exninfo -> message

of_exninfo exninfo prints the (Ltac2 and OCaml) backtrace info if it was recorded.

val concat : message -> message -> message

concat m1 m2 concatenates two messages.

Boxing primitives

They are translated to OCaml "Format" boxes, see https://ocaml.org/docs/formatting-text.

val force_new_line : message

force_new_line forces writing on a new line after this.

Warning: partially reinitializes the pretty-printing engine, potentially leading to bad printing afterwards. Prefer using a break hint inside a vertical box.

val break : int -> int -> message

General break hint: break n i either prints n spaces or splits the line adding i to the current indentation.

val space : message

Breaking space. Equivalent to break 1 0.

val hbox : message -> message

Horizontal box. Break hints in a horizontal box never split the line (nested boxes inside the horizontal box may allow line splitting).

val vbox : int -> message -> message

Vertical box. Every break hint in a vertical box splits the line. The int is added to the current indentation when splitting the line.

val hvbox : int -> message -> message

Horizontal/vertical box. Behaves as a horizontal box if it fits on a single line, otherwise behaves as a vertical box (using the given int).

val hovbox : int -> message -> message

Horizontal-or-vertical box. Prints as much as possible on each line, splitting the line at break hints when there is no more room on the line (see "Printing Width" option). The int is added to the indentation when splitting the line.