summaryrefslogtreecommitdiff
path: root/toplevel/cerrors.mli
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel/cerrors.mli')
-rw-r--r--toplevel/cerrors.mli11
1 files changed, 4 insertions, 7 deletions
diff --git a/toplevel/cerrors.mli b/toplevel/cerrors.mli
index c9cada8c..1768af11 100644
--- a/toplevel/cerrors.mli
+++ b/toplevel/cerrors.mli
@@ -1,24 +1,21 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Pp
-open Util
-
(** Error report. *)
-val print_loc : loc -> std_ppcmds
+val print_loc : Loc.t -> Pp.std_ppcmds
(** Pre-explain a vernac interpretation error *)
-val process_vernac_interp_error : exn -> exn
+val process_vernac_interp_error : 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 -> std_ppcmds
+val explain_exn_default : exn -> Pp.std_ppcmds