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, 14 insertions, 12 deletions

diff --git a/plugins/xml/acic2Xml.ml4 b/plugins/xml/acic2Xml.ml4
index 34bb1d51f..9d3a10dba 100644
--- a/plugins/xml/acic2Xml.ml4
+++ b/plugins/xml/acic2Xml.ml4
@@ -21,7 +21,7 @@ let typesdtdname = "http://mowgli.cs.unibo.it/dtd/cictypes.dtd";;
 
 let rec find_last_id =
  function
-    [] -> Errors.anomaly "find_last_id: empty list"
+    [] -> Errors.anomaly ~label:"find_last_id" (Pp.str "empty list")
   | [id,_,_] -> id
   | _::tl -> find_last_id tl
 ;;
diff --git a/plugins/xml/cic2acic.ml b/plugins/xml/cic2acic.ml
index 4a8436d76..2772779d4 100644
--- a/plugins/xml/cic2acic.ml
+++ b/plugins/xml/cic2acic.ml
@@ -12,6 +12,8 @@
 (*                       http://helm.cs.unibo.it                        *)
 (************************************************************************)
 
+open Pp
+
 (* Utility Functions *)
 
 exception TwoModulesWhoseDirPathIsOneAPrefixOfTheOther;;
@@ -162,7 +164,7 @@ let family_of_term ty =
  match Term.kind_of_term ty with
     Term.Sort s -> Coq_sort (Term.family_of_sort s)
   | Term.Const _ -> CProp  (* I could check that the constant is CProp *)
-  | _ -> Errors.anomaly "family_of_term"
+  | _ -> Errors.anomaly (Pp.str "family_of_term")
 ;;
 
 module CPropRetyping =
@@ -177,7 +179,7 @@ module CPropRetyping =
   | h::rest ->
       match T.kind_of_term (DoubleTypeInference.whd_betadeltaiotacprop env sigma typ) with
         | T.Prod (na,c1,c2) -> subst_type env sigma (T.subst1 h c2) rest
-        | _ -> Errors.anomaly "Non-functional construction"
+        | _ -> Errors.anomaly (Pp.str "Non-functional construction")
 
 
   let sort_of_atomic_type env sigma ft args =
@@ -193,7 +195,7 @@ let typeur sigma metamap =
     match Term.kind_of_term cstr with
     | T.Meta n ->
           (try T.strip_outer_cast (List.assoc n metamap)
-           with Not_found -> Errors.anomaly "type_of: this is not a well-typed term")
+           with Not_found -> Errors.anomaly ~label:"type_of" (Pp.str "this is not a well-typed term"))
     | T.Rel n ->
         let (_,_,ty) = Environ.lookup_rel n env in
         T.lift n ty
@@ -202,7 +204,7 @@ let typeur sigma metamap =
           let (_,_,ty) = Environ.lookup_named id env in
           ty
         with Not_found ->
-          Errors.anomaly ("type_of: variable "^(Names.Id.to_string id)^" unbound"))
+          Errors.anomaly ~label:"type_of" (str "variable " ++ Names.Id.print id ++ str " unbound"))
     | T.Const c ->
         let cb = Environ.lookup_constant c env in
         Typeops.type_of_constant_type env (cb.Declarations.const_type)
@@ -212,7 +214,7 @@ let typeur sigma metamap =
     | T.Case (_,p,c,lf) ->
         let Inductiveops.IndType(_,realargs) =
           try Inductiveops.find_rectype env sigma (type_of env c)
-          with Not_found -> Errors.anomaly "type_of: Bad recursive type" in
+          with Not_found -> Errors.anomaly ~label:"type_of" (Pp.str "Bad recursive type") in
         let t = Reductionops.whd_beta sigma (T.applist (p, realargs)) in
         (match Term.kind_of_term (DoubleTypeInference.whd_betadeltaiotacprop env sigma (type_of env t)) with
           | T.Prod _ -> Reductionops.whd_beta sigma (T.applist (t, [c]))
@@ -253,7 +255,7 @@ let typeur sigma metamap =
           | _, (CProp as s) -> s)
     | T.App(f,args) -> sort_of_atomic_type env sigma (type_of env f) args
     | T.Lambda _ | T.Fix _ | T.Construct _ ->
-        Errors.anomaly "sort_of: Not a type (1)"
+        Errors.anomaly ~label:"sort_of" (Pp.str "Not a type (1)")
     | _ -> outsort env sigma (type_of env t)
 
   and sort_family_of env t =
@@ -265,7 +267,7 @@ let typeur sigma metamap =
     | T.App(f,args) ->
        sort_of_atomic_type env sigma (type_of env f) args
     | T.Lambda _ | T.Fix _ | T.Construct _ ->
-        Errors.anomaly "sort_of: Not a type (1)"
+        Errors.anomaly ~label:"sort_of" (Pp.str "Not a type (1)")
     | _ -> outsort env sigma (type_of env t)
 
   in type_of, sort_of, sort_family_of
@@ -514,7 +516,7 @@ print_endline "PASSATO" ; flush stdout ;
                add_inner_type fresh_id'' ;
               A.AEvar
                (fresh_id'', n, Array.to_list (Array.map (aux' env idrefs) l))
-           | T.Meta _ -> Errors.anomaly "Meta met during exporting to XML"
+           | T.Meta _ -> Errors.anomaly (Pp.str "Meta met during exporting to XML")
            | T.Sort s -> A.ASort (fresh_id'', s)
            | T.Cast (v,_, t) ->
               Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
diff --git a/plugins/xml/xmlcommand.ml b/plugins/xml/xmlcommand.ml
index e16f9dd19..479b04228 100644
--- a/plugins/xml/xmlcommand.ml
+++ b/plugins/xml/xmlcommand.ml
@@ -289,7 +289,7 @@ let kind_of_variable id =
     | IsAssumption Conjectural -> "VARIABLE","Conjecture"
     | IsDefinition Definition -> "VARIABLE","LocalDefinition"
     | IsProof _ -> "VARIABLE","LocalFact"
-    | _ -> Errors.anomaly "Unsupported variable kind"
+    | _ -> Errors.anomaly (Pp.str "Unsupported variable kind")
 ;;
 
 let kind_of_constant kn =
@@ -423,7 +423,7 @@ let print_ref qid fn =
 (* pretty prints via Xml.pp the proof in progress on dest     *)
 let show_pftreestate internal fn (kind,pftst) id =
  if true then
-   Errors.anomaly "Xmlcommand.show_pftreestate is not supported in this version."
+   Errors.anomaly (Pp.str "Xmlcommand.show_pftreestate is not supported in this version.")
 
 let show fn =
  let pftst = Pfedit.get_pftreestate () in
@@ -519,7 +519,7 @@ let _ =
 	  let options = " --html -s --body-only --no-index --latin1 --raw-comments" in
           let command cmd =
            if Sys.command cmd <> 0 then
-            Errors.anomaly ("Error executing \"" ^ cmd ^ "\"")
+            Errors.anomaly (Pp.str ("Error executing \"" ^ cmd ^ "\""))
           in
            command (coqdoc^options^" -o "^fn^".xml "^fn^".v");
            command ("rm "^fn^".v "^fn^".glob");