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 errorpp
with optional header and locationloc
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, such as anomalies or interruptions should not be caught and ignored by mistake by inner Coq functions by means of doing a "catch-all". They should be handled instead by the compiler layer which is in charge of coordinating the intepretation of Coq vernaculars.
Please, avoid exceptions catch-all! If you must do so, then use the form:
try my_comp () with exn when noncritical exn -> my_handler
If you need to re-raise the excepction, you must work to preserve the backtrace and other important information:
try my_comp () with exn when noncritical exn -> let iexn = Exninfo.capture exn in ... Exninfo.iraise iexn
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