Module `CErrors`

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

Error handling

val push : exn -> Exninfo.iexn

Generic errors.

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

val anomaly : ?⁠loc:Loc.t -> ?⁠info:Exninfo.info -> ?⁠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 Pp.t: Main error signaling exception. It carries a header plus a pretty printing doc

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

exception Timeout

val register_handler : (exn -> Pp.t option) -> unit
val print : 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 register_additional_error_info : (Exninfo.info -> Pp.t option) -> unit: Register a printer for errors carrying additional information on exceptions. This method is fragile and should be considered deprecated