summaryrefslogtreecommitdiff
path: root/toplevel/explainErr.mli
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel/explainErr.mli')
-rw-r--r--toplevel/explainErr.mli21
1 files changed, 0 insertions, 21 deletions
diff --git a/toplevel/explainErr.mli b/toplevel/explainErr.mli
deleted file mode 100644
index a67c887a..00000000
--- a/toplevel/explainErr.mli
+++ /dev/null
@@ -1,21 +0,0 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
-
-(** Toplevel Exception *)
-exception EvaluatedError of Pp.std_ppcmds * exn option
-
-(** Pre-explain a vernac interpretation error *)
-
-val process_vernac_interp_error : ?allow_uncaught:bool -> ?with_header: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 register_additional_error_info : (Util.iexn -> (Pp.std_ppcmds option * Loc.t) option) -> unit