package coq-core
The Coq Proof Assistant -- Core Binaries and Tools
Install
Dune Dependency
Authors
Maintainers
Sources
coq-8.20.1.tar.gz
md5=0cfaa70f569be9494d24c829e6555d46
sha512=8ee967c636b67b22a4f34115871d8f9b9114df309afc9ddf5f61275251088c6e21f6cf745811df75554d30f4cebb6682f23eeb2e88b771330c4b60ce3f6bf5e2
doc/coq-core.printing/Genprint/index.html
Module GenprintSource
Entry point for generic printers
Source
type 'a with_level = {default_already_surrounded : Constrexpr.entry_relative_level;default_ensure_surrounded : Constrexpr.entry_relative_level;printer : 'a;
}Source
type printer_result = | PrinterBasic of Environ.env -> Evd.evar_map -> Pp.t| PrinterNeedsLevel of (Environ.env -> Evd.evar_map -> Constrexpr.entry_relative_level -> Pp.t) with_level
Source
type printer_fun_with_level =
Environ.env ->
Evd.evar_map ->
Constrexpr.entry_relative_level ->
Pp.tSource
type top_printer_result = | TopPrinterBasic of unit -> Pp.t| TopPrinterNeedsContext of Environ.env -> Evd.evar_map -> Pp.t| TopPrinterNeedsContextAndLevel of printer_fun_with_level with_level
Printer for raw level generic arguments.
Printer for glob level generic arguments.
Printer for top level generic arguments.
Source
val register_print0 :
('raw, 'glb, 'top) Genarg.genarg_type ->
'raw printer ->
'glb printer ->
'top top_printer ->
unit