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 Pp.t

Main error signaling exception. It carries a header plus a pretty printing doc

val user_err : ?⁠loc:Loc.t -> ?⁠ -> 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 : ( -> 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