Tac2print (u.3758aa3ddc38cffa23da0eeb3fa7893a.rocq-runtime.9.0.0.doc.ltac2_plugin.Ltac2

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

Sourcetype typ_level =

Sourceval pr_typref : Tac2expr.type_constant -> Pp.t

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

Sourceval pr_glbtype : ('a -> string) -> 'a Tac2expr.glb_typexpr -> Pp.t

Sourceval pr_constructor : Tac2expr.ltac_constructor -> Pp.t

Sourceval pr_internal_constructor : Tac2expr.type_constant -> int -> bool -> Pp.t

Sourceval pr_projection : Tac2expr.ltac_projection -> Pp.t

val pr_glbexpr_gen : 
  Tac2expr.exp_level ->
  avoid:Names.Id.Set.t ->
  Tac2expr.glb_tacexpr ->
  Pp.t

Sourceval pr_glbexpr : avoid:Names.Id.Set.t -> Tac2expr.glb_tacexpr -> Pp.t

Sourceval 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

Sourceval partial_pat_of_glb_pat : Tac2expr.glb_pat -> Tac2expr.PartialPat.t

Utility function

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

Sourcetype val_printer = {

}

Sourceval register_val_printer : Tac2expr.type_constant -> val_printer -> unit

val pr_valexpr : 
  Environ.env ->
  Evd.evar_map ->
  Tac2val.valexpr ->
  'a Tac2expr.glb_typexpr ->
  Pp.t

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

Sourcetype format =

Sourceval val_format : format list Tac2dyn.Val.tag

Sourceexception InvalidFormat

Sourceval parse_format : string -> format list