diff options
Diffstat (limited to 'lib/errors.mli')
| -rw-r--r-- | lib/errors.mli | 10 |
1 files changed, 9 insertions, 1 deletions
diff --git a/lib/errors.mli b/lib/errors.mli index 3dd470a06..0b2defa1a 100644 --- a/lib/errors.mli +++ b/lib/errors.mli @@ -16,11 +16,16 @@ open Pp [Anomaly] is used for system errors and [UserError] for the user's ones. *) -exception Anomaly of string * std_ppcmds +val make_anomaly : ?label:string -> std_ppcmds -> exn +(** Create an anomaly. *) + val anomaly : string -> 'a val anomalylabstrm : string -> std_ppcmds -> 'a val anomaly_loc : Loc.t * string * std_ppcmds -> 'a +val is_anomaly : exn -> bool +(** Check whether a given exception is an anomaly. *) + exception UserError of string * std_ppcmds val error : string -> 'a val errorlabstrm : string -> std_ppcmds -> 'a @@ -70,6 +75,9 @@ val register_handler : (exn -> Pp.std_ppcmds) -> unit (** The standard exception printer *) val print : exn -> Pp.std_ppcmds +(** Exception printer dedicated to anomalies. *) +val print_anomaly : exn -> Pp.std_ppcmds + (** Same as [print], except that the "Please report" part of an anomaly isn't printed (used in Ltac debugging). *) val print_no_report : exn -> Pp.std_ppcmds |