diff options
Diffstat (limited to 'toplevel/cerrors.mli')
| -rw-r--r-- | toplevel/cerrors.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/toplevel/cerrors.mli b/toplevel/cerrors.mli index 68c46010b5..a0e3e3c199 100644 --- a/toplevel/cerrors.mli +++ b/toplevel/cerrors.mli @@ -19,3 +19,4 @@ val process_vernac_interp_error : ?allow_uncaught:bool -> ?with_header:bool -> U val explain_exn_default : exn -> Pp.std_ppcmds +val register_additional_error_info : (Util.iexn -> (Pp.std_ppcmds option * Loc.t) option) -> unit |