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.19.0.tar.gz

md5=64b49dbc3205477bd7517642c0b9cbb6

sha512=02fb5b4fb575af79e092492cbec6dc0d15a1d74a07f827f657a72d4e6066532630e5a6d15be4acdb73314bd40b9a321f9ea0584e0ccfe51fd3a56353bd30db9b

doc/coq-core.vernac/Topfmt/index.html

Module `Topfmt`Source

Console printing options

Sourcetype pp_global_params = {

margin : int;
max_indent : int;
max_depth : int;
ellipsis : string;

}

Sourceval dflt_gp : pp_global_params

Sourceval deep_gp : pp_global_params

Sourceval set_gp : Format.formatter -> pp_global_params -> unit

Sourceval set_dflt_gp : Format.formatter -> unit

Sourceval get_gp : Format.formatter -> pp_global_params

Output functions of pretty-printing.

Sourceval with_output_to : out_channel -> Format.formatter

Sourceval std_ft : Format.formatter ref

Sourceval err_ft : Format.formatter ref

Sourceval deep_ft : Format.formatter ref

For parametrization through vernacular.

Sourceval set_depth_boxes : int option -> unit

Sourceval get_depth_boxes : unit -> int option

Sourceval set_margin : int option -> unit

Sourceval get_margin : unit -> int option

Sourceval std_logger : ?pre_hdr:Pp.t -> Feedback.level -> Pp.t -> unit

Console display of feedback, we may add some location information

Sourceval emacs_logger : ?pre_hdr:Pp.t -> Feedback.level -> Pp.t -> unit

Sourceval default_styles : unit -> unit

Color output

Sourceval parse_color_config : string -> unit

Sourceval dump_tags : unit -> (string * Terminal.style) list

Sourceval set_emacs_print_strings : unit -> unit

Sourceval init_terminal_output : color:bool -> unit

Initialization of interpretation of tags

Error printing

Sourcetype execution_phase =

| ParsingCommandLine
| Initialization
| LoadingPrelude
| LoadingRcFile
| InteractiveLoop
| CompilationPhase

Sourceval in_phase : phase:execution_phase -> ('a -> 'b) -> 'a -> 'b

Sourceval pr_phase : ?loc:Loc.t -> unit -> Pp.t option

Sourceval print_err_exn : exn -> unit

Sourceval with_output_to_file : string -> ('a -> 'b) -> 'a -> 'b

with_output_to_file file f x executes f x with logging redirected to a file file

Sourceval pr_cmd_header : Vernacexpr.vernac_control -> Pp.t

On This Page

Output functions of pretty-printing.
For parametrization through vernacular.