Module Ltac2_plugin.Tac2print

val pr_tacref : Tac2expr.ltac_constant -> Pp.t

Prints the shortest name for the constant. Also works for constants not in the nametab (because they're local to another module).

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
val pr_partial_pat : Tac2expr.PartialPat.t -> Pp.t
val partial_pat_of_glb_pat : Tac2expr.glb_pat -> Tac2expr.PartialPat.t

Utility function

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
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.

Ltac2 primitives
type format =
| FmtString
| FmtInt
| FmtConstr
| FmtIdent
| FmtLiteral of string
| FmtAlpha
val val_format : format list Tac2dyn.Val.tag
exception InvalidFormat
val parse_format : string -> format list