Uniformization of the "anomaly" command.

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

1 files changed, 6 insertions, 7 deletions

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)