1 files changed, 36 insertions, 0 deletions
diff --git a/lib/errors.mli b/lib/errors.mli
index eb7fde8e77..a863c5e30e 100644
--- a/lib/errors.mli
+++ b/lib/errors.mli
@@ -6,9 +6,45 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
+open Pp
+
 (** This modules implements basic manipulations of errors for use
     throughout Coq's code. *)
 
+(** {6 Generic errors.}
+
+ [Anomaly] is used for system errors and [UserError] for the
+   user's ones. *)
+
+exception Anomaly of string * std_ppcmds
+val anomaly : string -> 'a
+val anomalylabstrm : string -> std_ppcmds -> 'a
+val anomaly_loc : loc * string * std_ppcmds -> 'a
+
+exception UserError of string * std_ppcmds
+val error : string -> 'a
+val errorlabstrm : string -> std_ppcmds -> 'a
+val user_err_loc : loc * string * std_ppcmds -> 'a
+
+exception AlreadyDeclared of std_ppcmds
+val alreadydeclared : std_ppcmds -> 'a
+
+val invalid_arg_loc : loc * string -> 'a
+
+(** [todo] is for running of an incomplete code its implementation is
+   "do nothing" (or print a message), but this function should not be
+   used in a released code *)
+
+val todo : string -> unit
+
+exception Timeout
+
+(** Like [Exc_located], but specifies the outermost file read, the
+   input buffer associated to the location of the error (or the module name
+   if boolean is true), and the error itself. *)
+
+exception Error_in_file of string * (bool * string * loc) * exn
+
 (** [register_handler h] registers [h] as a handler.
     When an expression is printed with [print e], it
     goes through all registered handles (the most