package coq-core

You can search for identifiers within the package.

in-package search v0.2.0

The Coq Proof Assistant -- Core Binaries and Tools

Install

Dune Dependency

coq.inria.fr Readme Edit opam file Versions (9)

Authors

T

The Coq development team, INRIA, CNRS, and contributors

Maintainers

T

The Coq development team <coqdev@inria.fr>

Sources

coq-8.17.0.tar.gz

sha512=2f77bcb5211018b5d46320fd39fd34450eeb654aca44551b28bb50a2364398c4b34587630b6558db867ecfb63b246fd3e29dc2375f99967ff62bc002db9c3250

doc/ltac2_plugin/Ltac2_plugin/Tac2print/index.html

Module `Ltac2_plugin.Tac2print`Source

Sourceval 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

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

Sourceval pr_partial_pat : Tac2expr.PartialPat.t -> Pp.t

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

Utility function

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

On This Page

Printing types
Printing expressions
Printing values
Utilities
Ltac2 primitives