package coq-core

  1. Overview
  2. Docs
The Coq Proof Assistant -- Core Binaries and Tools

Install 

dune-project
 Dependency

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

Authors

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

Maintainers

  1. T
    The Coq development team <coqdev@inria.fr>

Sources

coq-8.20.1.tar.gz
md5=0cfaa70f569be9494d24c829e6555d46
sha512=8ee967c636b67b22a4f34115871d8f9b9114df309afc9ddf5f61275251088c6e21f6cf745811df75554d30f4cebb6682f23eeb2e88b771330c4b60ce3f6bf5e2

doc/ltac2_plugin/Ltac2_plugin/Tac2print/index.html

Module Ltac2_plugin.Tac2printSource

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 =
  1. | T5_l
  2. | T5_r
  3. | T2
  4. | T1
  5. | T0
Sourceval 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 : avoid:Names.Id.Set.t -> 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 = {
  1. 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
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 =
  1. | FmtString
  2. | FmtInt
  3. | FmtConstr
  4. | FmtIdent
  5. | FmtLiteral of string
  6. | FmtAlpha
Sourceval val_format : format list Tac2dyn.Val.tag
Sourceexception InvalidFormat
Sourceval parse_format : string -> format list