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 -> ?⁠ -> ?⁠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 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 : ( -> Pp.t Loc.located option) -> unit

Register a printer for errors carrying additional information on exceptions. This method is fragile and should be considered deprecated