aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac/explainErr.mli
diff options
context:
space:
mode:
Diffstat (limited to 'vernac/explainErr.mli')
-rw-r--r--vernac/explainErr.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/explainErr.mli b/vernac/explainErr.mli
index 370ad7e3b..9202729ce 100644
--- a/vernac/explainErr.mli
+++ b/vernac/explainErr.mli
@@ -18,4 +18,4 @@ val process_vernac_interp_error : ?allow_uncaught:bool -> Util.iexn -> Util.iexn
val explain_exn_default : exn -> Pp.std_ppcmds
-val register_additional_error_info : (Util.iexn -> (Pp.std_ppcmds option * Loc.t) option) -> unit
+val register_additional_error_info : (Util.iexn -> (Pp.std_ppcmds option Loc.located) option) -> unit