Uniformization of the "anomaly" command.

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

3 files changed, 10 insertions, 11 deletions

diff --git a/lib/dyn.ml b/lib/dyn.ml
index de5158b141..aec7071235 100644
--- a/lib/dyn.ml
+++ b/lib/dyn.ml
@@ -16,7 +16,7 @@ let dyntab = ref ([] : string list)
 
 let create s =
   if List.mem s !dyntab then
-    anomaly ("Dyn.create: already declared dynamic " ^ s);
+    anomaly ~label:"Dyn.create" (Pp.str ("already declared dynamic " ^ s));
   dyntab := s :: !dyntab;
   ((fun v -> (s,Obj.repr v)),
    (fun (s',rv) ->
diff --git a/lib/errors.ml b/lib/errors.ml
index d4d285a053..342ec10225 100644
--- a/lib/errors.ml
+++ b/lib/errors.ml
@@ -26,8 +26,12 @@ let anomaly_gen label pp =
   let bt = get_backtrace () in
   raise (Anomaly (label, pp, bt))
 
-let anomaly string =
-  anomaly_gen None (str string)
+let anomaly ?loc ?label pp =
+  let bt = get_backtrace () in
+  match loc with
+  | None -> raise (Anomaly (label, pp, bt))
+  | Some loc ->
+    Loc.raise loc (Anomaly (label, pp, bt))
 
 let anomalylabstrm string pps =
   anomaly_gen (Some string) pps
@@ -45,11 +49,6 @@ let alreadydeclared pps = raise (AlreadyDeclared(pps))
 
 let todo s = prerr_string ("TODO: "^s^"\n")
 
-(* raising located exceptions *)
-let anomaly_loc (loc,s,strm) =
-  let bt = get_backtrace () in
-  Loc.raise loc (Anomaly (Some s, strm, bt))
-
 let user_err_loc (loc,s,strm) = Loc.raise loc (UserError (s,strm))
 let invalid_arg_loc (loc,s) = Loc.raise loc (Invalid_argument s)
 
diff --git a/lib/errors.mli b/lib/errors.mli
index 0b2defa1a0..00c39c2b3d 100644
--- a/lib/errors.mli
+++ b/lib/errors.mli
@@ -19,9 +19,9 @@ open Pp
 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 anomaly : ?loc:Loc.t -> ?label:string -> std_ppcmds -> 'a
+(** Raise an anomaly, with an optional location and an optional
+    label identifying the anomaly. *)
 
 val is_anomaly : exn -> bool
 (** Check whether a given exception is an anomaly. *)