package coq

Overview
No Docs

You can search for identifiers within the package.

in-package search v0.2.0

On This Page

Printing types
Printing expressions
Printing values
Utilities
Ltac2 primitives

Formal proof management system

Install

dune-project

Dependency

coq.inria.fr Edit opam file Versions (40)

Authors

T

The Coq development team, INRIA, CNRS, and contributors.

Maintainers

C

coqdev@inria.fr

Sources

coq-8.14.1.tar.gz

sha256=3cbfc1e1a72b16d4744f5b64ede59586071e31d9c11c811a0372060727bfd9c3

doc/ltac2_plugin/Ltac2_plugin/Tac2print/index.html

Module `Ltac2_plugin.Tac2print`Source

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

Sourceval pr_glbexpr_gen : Tac2expr.exp_level -> Tac2expr.glb_tacexpr -> Pp.t

Sourceval pr_glbexpr : Tac2expr.glb_tacexpr -> Pp.t

Printing values

Sourcetype val_printer = {

val_printer : 'a. Environ.env -> Evd.evar_map -> Tac2ffi.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 ->
  Tac2ffi.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