Module `Ltac2_plugin.Tac2print`

val pr_tacref : Names.Id.Set.t -> 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).

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

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 -> avoid:Names.Id.Set.t -> Tac2expr.glb_tacexpr -> Pp.t
val pr_glbexpr : avoid:Names.Id.Set.t -> Tac2expr.glb_tacexpr -> Pp.t
val pr_partial_pat : Tac2expr.PartialPat.t -> Pp.t
val pr_rawexpr_gen : Tac2expr.exp_level -> avoid:Names.Id.Set.t -> Tac2expr.raw_tacexpr -> Pp.t
val partial_pat_of_glb_pat : Tac2expr.glb_pat -> Tac2expr.PartialPat.t: Utility function

val ids_of_pattern : Names.Id.Set.t -> Tac2expr.raw_patexpr -> Names.Id.Set.t

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

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.

type format = | FmtString | FmtInt | FmtConstr | FmtIdent | FmtLiteral of string | FmtAlpha