diff options
Diffstat (limited to 'lib/cErrors.mli')
| -rw-r--r-- | lib/cErrors.mli | 54 |
1 files changed, 26 insertions, 28 deletions
diff --git a/lib/cErrors.mli b/lib/cErrors.mli index e5dad93f..ec34dd62 100644 --- a/lib/cErrors.mli +++ b/lib/cErrors.mli @@ -1,12 +1,12 @@ -(***********************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) -(* \VV/ *************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(***********************************************************************) - -open Pp +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) (** This modules implements basic manipulations of errors for use throughout Coq's code. *) @@ -21,10 +21,10 @@ val push : exn -> Exninfo.iexn [Anomaly] is used for system errors and [UserError] for the user's ones. *) -val make_anomaly : ?label:string -> std_ppcmds -> exn +val make_anomaly : ?label:string -> Pp.t -> exn (** Create an anomaly. *) -val anomaly : ?loc:Loc.t -> ?label:string -> std_ppcmds -> 'a +val anomaly : ?loc:Loc.t -> ?label:string -> Pp.t -> 'a (** Raise an anomaly, with an optional location and an optional label identifying the anomaly. *) @@ -33,15 +33,18 @@ val is_anomaly : exn -> bool This is mostly provided for compatibility. Please avoid doing specific tricks with anomalies thanks to it. See rather [noncritical] below. *) -exception UserError of string * std_ppcmds -val error : string -> 'a -val errorlabstrm : string -> std_ppcmds -> 'a -val user_err_loc : Loc.t * string * std_ppcmds -> 'a +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 AlreadyDeclared of std_ppcmds -val alreadydeclared : std_ppcmds -> 'a +exception AlreadyDeclared of Pp.t +val alreadydeclared : Pp.t -> 'a -val invalid_arg_loc : Loc.t * string -> 'a +val invalid_arg : ?loc:Loc.t -> string -> 'a (** [todo] is for running of an incomplete code its implementation is "do nothing" (or print a message), but this function should not be @@ -71,16 +74,16 @@ exception Quit exception Unhandled -val register_handler : (exn -> Pp.std_ppcmds) -> unit +val register_handler : (exn -> Pp.t) -> unit (** The standard exception printer *) -val print : ?info:Exninfo.info -> exn -> Pp.std_ppcmds -val iprint : Exninfo.iexn -> Pp.std_ppcmds +val print : ?info:Exninfo.info -> exn -> Pp.t +val iprint : Exninfo.iexn -> Pp.t (** 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 -val iprint_no_report : Exninfo.iexn -> Pp.std_ppcmds +val print_no_report : exn -> Pp.t +val iprint_no_report : Exninfo.iexn -> Pp.t (** Critical exceptions should not be caught and ignored by mistake by inner functions during a [vernacinterp]. They should be handled @@ -92,8 +95,3 @@ val noncritical : exn -> bool (** Check whether an exception is handled by some toplevel printer. The [Anomaly] exception is never handled. *) val handled : exn -> bool - -(** Prints info which is either an error or - an anomaly and then exits with the appropriate - error code *) -val fatal_error : Pp.std_ppcmds -> bool -> 'a |