Module `CErrors`

This modules implements basic manipulations of errors for use throughout Coq's code.

Error handling

val push : exn -> Exninfo.iexn: Alias for Backtrace.add_backtrace.

Generic errors.

Anomaly is used for system errors and UserError for the user's ones.

val make_anomaly : ?⁠label:string -> Pp.t -> exn: Create an anomaly.

val anomaly : ?⁠loc:Loc.t -> ?⁠label:string -> Pp.t -> 'a: Raise an anomaly, with an optional location and an optional label identifying the anomaly.

val is_anomaly : exn -> bool: Check whether a given exception is an anomaly. This is mostly provided for compatibility. Please avoid doing specific tricks with anomalies thanks to it. See rather noncritical below.

exception UserError of string option * Pp.t: Main error signaling exception. It carries a header plus a pretty printing doc

val user_err : ?⁠loc:Loc.t -> ?⁠hdr:string -> Pp.t -> 'a: Main error raising primitive. user_err ?loc ?hdr pp signals an error pp with optional header and location hdr loc

exception AlreadyDeclared of Pp.t

val alreadydeclared : Pp.t -> 'a
val invalid_arg : ?⁠loc:Loc.t -> string -> 'a

val todo : string -> unit

exception Timeout

exception Unhandled

val register_handler : (exn -> Pp.t) -> unit
val print : ?⁠info:Exninfo.info -> exn -> Pp.t: The standard exception printer

val iprint : Exninfo.iexn -> Pp.t
val print_no_report : exn -> Pp.t: Same as print, except that the "Please report" part of an anomaly isn't printed (used in Ltac debugging).

val iprint_no_report : Exninfo.iexn -> Pp.t
val noncritical : exn -> bool: Critical exceptions should not be caught and ignored by mistake by inner functions during a vernacinterp. They should be handled only in Toplevel.do_vernac (or Ideslave), to be displayed to the user. Typical example: Sys.Break, Assert_failure, Anomaly ...

val handled : exn -> bool: Check whether an exception is handled by some toplevel printer. The Anomaly exception is never handled.