package coq-core

  1. Overview
  2. Docs
package coq-core
Legend:
Library
Module
Module type
Parameter
Class
Class type

Entry point for generic printers

type 'a with_level = {
  1. default_already_surrounded : Constrexpr.entry_relative_level;
  2. default_ensure_surrounded : Constrexpr.entry_relative_level;
  3. printer : 'a;
}
type printer_result =
  1. | PrinterBasic of Environ.env -> Evd.evar_map -> Pp.t
  2. | PrinterNeedsLevel of (Environ.env -> Evd.evar_map -> Constrexpr.entry_relative_level -> Pp.t) with_level
type printer_fun_with_level = Environ.env -> Evd.evar_map -> Constrexpr.entry_relative_level -> Pp.t
type top_printer_result =
  1. | TopPrinterBasic of unit -> Pp.t
  2. | TopPrinterNeedsContext of Environ.env -> Evd.evar_map -> Pp.t
  3. | TopPrinterNeedsContextAndLevel of printer_fun_with_level with_level
type 'a printer = 'a -> printer_result
type 'a top_printer = 'a -> top_printer_result
val raw_print : ('raw, 'glb, 'top) Genarg.genarg_type -> 'raw printer

Printer for raw level generic arguments.

val glb_print : ('raw, 'glb, 'top) Genarg.genarg_type -> 'glb printer

Printer for glob level generic arguments.

val top_print : ('raw, 'glb, 'top) Genarg.genarg_type -> 'top top_printer

Printer for top level generic arguments.

val register_print0 : ('raw, 'glb, 'top) Genarg.genarg_type -> 'raw printer -> 'glb printer -> 'top top_printer -> unit
val register_val_print0 : 'top Geninterp.Val.typ -> 'top top_printer -> unit
val register_vernac_print0 : ('raw, 'glb, 'top) Genarg.genarg_type -> 'raw printer -> unit
val generic_val_print : Geninterp.Val.t top_printer
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct