diff options
| author | Emilio Jesus Gallego Arias | 2019-07-01 00:16:40 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-07-08 13:12:05 +0200 |
| commit | b372c0cf33681ef7e8ae3524987c5581fd3f92c0 (patch) | |
| tree | a7da4cf538f3a481995ad86bdd7aa18822bccf8b /lib/cErrors.mli | |
| parent | a5e4dd7faa23abd4a4ebe093076484d090a8a47e (diff) | |
[errors] Small cleanups and removal of dead code.
Diffstat (limited to 'lib/cErrors.mli')
| -rw-r--r-- | lib/cErrors.mli | 13 |
1 files changed, 1 insertions, 12 deletions
diff --git a/lib/cErrors.mli b/lib/cErrors.mli index 100dcd0b22..02eaf6bd0b 100644 --- a/lib/cErrors.mli +++ b/lib/cErrors.mli @@ -21,9 +21,6 @@ val push : exn -> Exninfo.iexn [Anomaly] is used for system errors and [UserError] for the user's ones. *) -val make_anomaly : ?label:string -> Pp.t -> exn -(** Create an anomaly. *) - val anomaly : ?loc:Loc.t -> ?label:string -> Pp.t -> 'a (** Raise an anomaly, with an optional location and an optional label identifying the anomaly. *) @@ -41,14 +38,6 @@ 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] *) -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 - used in a released code *) - -val todo : string -> unit - exception Timeout (** [register_handler h] registers [h] as a handler. @@ -72,7 +61,7 @@ exception Unhandled val register_handler : (exn -> Pp.t) -> unit (** The standard exception printer *) -val print : ?info:Exninfo.info -> exn -> Pp.t +val print : exn -> Pp.t val iprint : Exninfo.iexn -> Pp.t (** Same as [print], except that the "Please report" part of an anomaly |
