Added backtrace information to anomalies

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16161 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 9 insertions, 1 deletions

diff --git a/lib/errors.mli b/lib/errors.mli
index 3dd470a064..0b2defa1a0 100644
--- a/lib/errors.mli
+++ b/lib/errors.mli
@@ -16,11 +16,16 @@ open Pp
  [Anomaly] is used for system errors and [UserError] for the
    user's ones. *)
 
-exception Anomaly of string * std_ppcmds
+val make_anomaly : ?label:string -> std_ppcmds -> exn
+(** Create an anomaly. *)
+
 val anomaly : string -> 'a
 val anomalylabstrm : string -> std_ppcmds -> 'a
 val anomaly_loc : Loc.t * string * std_ppcmds -> 'a
 
+val is_anomaly : exn -> bool
+(** Check whether a given exception is an anomaly. *)
+
 exception UserError of string * std_ppcmds
 val error : string -> 'a
 val errorlabstrm : string -> std_ppcmds -> 'a
@@ -70,6 +75,9 @@ val register_handler : (exn -> Pp.std_ppcmds) -> unit
 (** The standard exception printer *)
 val print : exn -> Pp.std_ppcmds
 
+(** Exception printer dedicated to anomalies. *)
+val print_anomaly : exn -> Pp.std_ppcmds
+
 (** Same as [print], except that the "Please report" part of an anomaly
     isn't printed (used in Ltac debugging). *)
 val print_no_report : exn -> Pp.std_ppcmds