diff options
Diffstat (limited to 'lib/errors.mli')
| -rw-r--r-- | lib/errors.mli | 6 |
1 files changed, 0 insertions, 6 deletions
diff --git a/lib/errors.mli b/lib/errors.mli index 5f230d4c3b..c5400574b8 100644 --- a/lib/errors.mli +++ b/lib/errors.mli @@ -51,12 +51,6 @@ exception Timeout exception Drop exception Quit -(** Like [Exc_located], but specifies the outermost file read, the - input buffer associated to the location of the error (or the module name - if boolean is true), and the error itself. *) - -exception Error_in_file of string * (bool * string * Loc.t) * exn - (** [register_handler h] registers [h] as a handler. When an expression is printed with [print e], it goes through all registered handles (the most |