Uniformization of the "anomaly" command.

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

4 files changed, 12 insertions, 11 deletions

diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml
index 59768f5a68..4fc251edc0 100644
--- a/parsing/egramcoq.ml
+++ b/parsing/egramcoq.ml
@@ -145,7 +145,7 @@ let make_cases_pattern_action
 	Gram.action (fun (v:local_binder list list) ->
 	  make (env, envlist, true) tl)
     | (ETPattern | ETOther _) ->
-        anomaly "Unexpected entry of type cases pattern or other")
+        anomaly (Pp.str "Unexpected entry of type cases pattern or other"))
   | GramConstrListMark (n,b) :: tl ->
       (* Rebuild expansions of ConstrList *)
       let heads,env = List.chop n env in
diff --git a/parsing/extrawit.ml b/parsing/extrawit.ml
index 3e1c44e5a5..b36e39079d 100644
--- a/parsing/extrawit.ml
+++ b/parsing/extrawit.ml
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Pp
 open Genarg
 
 (* This file defines extra argument types *)
@@ -28,7 +29,7 @@ let wit_tactic = function
   | 3 -> wit_tactic3
   | 4 -> wit_tactic4
   | 5 -> wit_tactic5
-  | n -> Errors.anomaly ("Unavailable tactic level: "^string_of_int n)
+  | n -> Errors.anomaly (str "Unavailable tactic level:" ++ spc () ++ int n)
 
 let globwit_tactic = function
   | 0 -> globwit_tactic0
@@ -37,7 +38,7 @@ let globwit_tactic = function
   | 3 -> globwit_tactic3
   | 4 -> globwit_tactic4
   | 5 -> globwit_tactic5
-  | n -> Errors.anomaly ("Unavailable tactic level: "^string_of_int n)
+  | n -> Errors.anomaly (str "Unavailable tactic level:" ++ spc () ++ int n)
 
 let rawwit_tactic = function
   | 0 -> rawwit_tactic0
@@ -46,7 +47,7 @@ let rawwit_tactic = function
   | 3 -> rawwit_tactic3
   | 4 -> rawwit_tactic4
   | 5 -> rawwit_tactic5
-  | n -> Errors.anomaly ("Unavailable tactic level: "^string_of_int n)
+  | n -> Errors.anomaly (str "Unavailable tactic level:" ++ spc () ++ int n)
 
 let tactic_genarg_level s =
   if Int.equal (String.length s) 7 && String.sub s 0 6 = "tactic" then
diff --git a/parsing/g_xml.ml4 b/parsing/g_xml.ml4
index 53ade7c2c3..372f92eed1 100644
--- a/parsing/g_xml.ml4
+++ b/parsing/g_xml.ml4
@@ -98,7 +98,7 @@ let global_of_cdata (loc,a) = Nametab.locate (uri_of_data a)
 
 let inductive_of_cdata a = match global_of_cdata a with
     | IndRef (kn,_) -> kn
-    | _ -> anomaly "XML parser: not an inductive"
+    | _ -> anomaly ~label:"XML parser" (str "not an inductive")
 
 let ltacref_of_cdata (loc,a) = (loc,locate_tactic (uri_of_data a))
 
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index b7d2c844f3..e66458ebea 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -117,7 +117,7 @@ struct
   let inGramObj rawwit = in_typed_entry (unquote rawwit)
   let outGramObj (a:'a raw_abstract_argument_type) o =
     if not (argument_type_eq (type_of_typed_entry o) (unquote a))
-      then anomaly "outGramObj: wrong type";
+      then anomaly ~label:"outGramObj" (str "wrong type");
     (* downcast from grammar_object *)
     Obj.magic (object_of_typed_entry o)
 end
@@ -209,7 +209,7 @@ let grammar_extend e reinit ext =
 let rec remove_grammars n =
   if n>0 then
     (match !camlp4_state with
-       | [] -> anomaly "Pcoq.remove_grammars: too many rules to remove"
+       | [] -> anomaly ~label:"Pcoq.remove_grammars" (Pp.str "too many rules to remove")
        | ByGrammar(g,reinit,ext)::t ->
            grammar_delete g (Option.map of_coq_assoc reinit) ext;
            camlp4_state := t;
@@ -266,7 +266,7 @@ let get_univ s =
   try
     Hashtbl.find univ_tab s
   with Not_found ->
-    anomaly ("Unknown grammar universe: "^s)
+    anomaly (Pp.str ("Unknown grammar universe: "^s))
 
 let get_entry (u, utab) s = Hashtbl.find utab s
 
@@ -621,16 +621,16 @@ let compute_entry allow_create adjust forpat = function
        else weaken_entry Constr.operconstr),
       adjust (n,q), false
   | ETName -> weaken_entry Prim.name, None, false
-  | ETBinder true -> anomaly "Should occur only as part of BinderList"
+  | ETBinder true -> anomaly (Pp.str "Should occur only as part of BinderList")
   | ETBinder false -> weaken_entry Constr.binder, None, false
   | ETBinderList (true,tkl) ->
     let () = match tkl with [] -> () | _ -> assert false in
     weaken_entry Constr.open_binders, None, false
-  | ETBinderList (false,_) -> anomaly "List of entries cannot be registered."
+  | ETBinderList (false,_) -> anomaly (Pp.str "List of entries cannot be registered.")
   | ETBigint -> weaken_entry Prim.bigint, None, false
   | ETReference -> weaken_entry Constr.global, None, false
   | ETPattern -> weaken_entry Constr.pattern, None, false
-  | ETConstrList _ -> anomaly "List of entries cannot be registered."
+  | ETConstrList _ -> anomaly (Pp.str "List of entries cannot be registered.")
   | ETOther (u,n) ->
       let u = get_univ u in
       let e =