aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac/explainErr.mli
diff options
context:
space:
mode:
Diffstat (limited to 'vernac/explainErr.mli')
-rw-r--r--vernac/explainErr.mli6
1 files changed, 3 insertions, 3 deletions
diff --git a/vernac/explainErr.mli b/vernac/explainErr.mli
index 944339d85..0cbd71fa4 100644
--- a/vernac/explainErr.mli
+++ b/vernac/explainErr.mli
@@ -7,7 +7,7 @@
(************************************************************************)
(** Toplevel Exception *)
-exception EvaluatedError of Pp.std_ppcmds * exn option
+exception EvaluatedError of Pp.t * exn option
(** Pre-explain a vernac interpretation error *)
@@ -16,6 +16,6 @@ val process_vernac_interp_error : ?allow_uncaught:bool -> Util.iexn -> Util.iexn
(** General explain function. Should not be used directly now,
see instead function [Errors.print] and variants *)
-val explain_exn_default : exn -> Pp.std_ppcmds
+val explain_exn_default : exn -> Pp.t
-val register_additional_error_info : (Util.iexn -> (Pp.std_ppcmds option Loc.located) option) -> unit
+val register_additional_error_info : (Util.iexn -> (Pp.t option Loc.located) option) -> unit