diff options
Diffstat (limited to 'lib/util.mli')
| -rw-r--r-- | lib/util.mli | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/lib/util.mli b/lib/util.mli index 58d5150b72..e4a2ef7075 100644 --- a/lib/util.mli +++ b/lib/util.mli @@ -41,6 +41,12 @@ val user_err_loc : loc * string * std_ppcmds -> 'a val invalid_arg_loc : loc * string -> 'a val join_loc : loc -> loc -> loc +(* 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) * exn + (*s Projections from triplets *) val pi1 : 'a * 'b * 'c -> 'a |