package coq-core

  1. Overview
  2. Docs
package coq-core
Legend:
Library
Module
Module type
Parameter
Class
Class type
type status =
  1. | Disabled
  2. | Enabled
  3. | AsError
type category

Categories and warnings form a DAG with a common root all and warnings as the leaves.

val all : category
type warning

Each warning belongs to some categories maybe including "default". It is possible to query the status of a warning (unlike categories). XXX we should probably have "default-error" too.

type 'a msg

A msg belongs to a warning.

val warn : 'a msg -> ?loc:Loc.t -> 'a -> unit

Emit a message in some warning.

Creation functions

Note that names are in a combined namespace including the special name "none".

val create_category : ?from:category list -> name:string -> unit -> category

When from is not specified it defaults to [all]. Empty list from is not allowed. "default" is not allowed in from.

val create_warning : ?from:category list -> ?default:status -> name:string -> unit -> warning

from works the same as with create_category. In particular default status is specified through the default argument not by using the "default" category.

val create_hybrid : ?from:category list -> ?default:status -> name:string -> unit -> category * warning

As create_warning, but the warning can also be used as a category i.e. have sub-warnings.

val create_msg : warning -> unit -> 'a msg

A message with data 'a in the given warning.

val create_in : warning -> ('a -> Pp.t) -> ?loc:Loc.t -> 'a -> unit

Create a msg with registered printer.

val register_printer : 'a msg -> ('a -> Pp.t) -> unit

Register the printer for a given message. If a printer is already registered it is replaced.

val create : name:string -> ?category:category -> ?default:status -> ('a -> Pp.t) -> ?loc:Loc.t -> 'a -> unit

Combined creation function. name must be a fresh name.

Misc APIs

val get_flags : unit -> string
val set_flags : string -> unit
type 'a elt =
  1. | There of 'a
  2. | NotThere
  3. | OtherType
val get_category : string -> category elt

Get preexisting category by name.

val get_warning : string -> warning elt

Get preexisting warning by name.

val warning_status : warning -> status

Current status of the warning.

val get_status : name:string -> status
val normalize_flags_string : string -> string

Cleans up a user provided warnings status string, e.g. removing unknown warnings (in which case a warning is emitted) or subsumed warnings .

val with_warn : string -> ('b -> 'a) -> 'b -> 'a

with_warn "-xxx,+yyy..." f x calls f x after setting the warnings as specified in the string (keeping other previously set warnings), and restores current warnings after f() returns or raises an exception. If both f and restoring the warnings raise exceptions, the latter is raised.

val check_unknown_warnings : string -> unit

Warn with "unknown-warning" if any unknown warnings are in the string with non-disabled status.

val override_unknown_warning : bool Stdlib.ref

For command line -w, this avoids using the warning system to avoid breaking "-w -unknown-warning".

  • deprecated Do not use, internal.
module CoreCategories : sig ... end

Categories used in coq-core. Might not be exhaustive.

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