Module `Ltac2_plugin.Tac2print`Source

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

Printing types

Sourcetype typ_level =

| T5_l
| T5_r
| T2
| T1
| T0

Sourceval pr_typref : Tac2expr.type_constant -> Pp.t

Source

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

Printing expressions

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

Source

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

Source

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

Printing values

Sourcetype val_printer = {

val_printer : 'a. Environ.env -> Evd.evar_map -> Tac2val.valexpr -> 'a Tac2expr.glb_typexpr list -> Pp.t;

}

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

Source

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

Utilities

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.

Ltac2 primitives

Sourcetype format =

| FmtString
| FmtInt
| FmtConstr
| FmtIdent
| FmtLiteral of string
| FmtAlpha

Sourceval val_format : format list Tac2dyn.Val.tag

Sourceexception InvalidFormat

Sourceval parse_format : string -> format list

Install

Dune Dependency

Authors

Maintainers

Sources

doc/ltac2_plugin/Ltac2_plugin/Tac2print/index.html

Module `Ltac2_plugin.Tac2print`Source

Printing types

Printing expressions

Printing values

Utilities

Ltac2 primitives

package rocq-runtime

Install

Dune Dependency

Authors

Maintainers

Sources

doc/ltac2_plugin/Ltac2_plugin/Tac2print/index.html

Module Ltac2_plugin.Tac2printSource

Printing types

Printing expressions

Printing values

Utilities

Ltac2 primitives

Module `Ltac2_plugin.Tac2print`Source