Module `Ltac2_plugin.Tac2print`

Printing types

type typ_level = | T5_l | T5_r | T2 | T1 | T0

val pr_typref : Tac2expr.type_constant -> Pp.t
val pr_glbtype_gen : ('a -> string) -> typ_level -> 'a Tac2expr.glb_typexpr -> Pp.t
val pr_glbtype : ('a -> string) -> 'a Tac2expr.glb_typexpr -> Pp.t

Printing expressions

val pr_constructor : Tac2expr.ltac_constructor -> Pp.t
val pr_internal_constructor : Tac2expr.type_constant -> int -> bool -> Pp.t
val pr_projection : Tac2expr.ltac_projection -> Pp.t
val pr_glbexpr_gen : Tac2expr.exp_level -> Tac2expr.glb_tacexpr -> Pp.t
val pr_glbexpr : Tac2expr.glb_tacexpr -> Pp.t

Printing values

type val_printer = { val_printer : a. Environ.env -> Evd.evar_map -> Tac2ffi.valexpr -> 'a Tac2expr.glb_typexpr list -> Pp.t; }

val register_val_printer : Tac2expr.type_constant -> val_printer -> unit
val pr_valexpr : Environ.env -> Evd.evar_map -> Tac2ffi.valexpr -> 'a Tac2expr.glb_typexpr -> Pp.t

Utilities

val int_name : unit -> int -> string: Create a function that give names to integers. The names are generated on the fly, in the order they are encountered.