Noise for nothing

Util only depends on Ocaml stdlib and Utf8 tables.
Generic pretty printing and loc functions are in Pp.
Generic errors are in Errors.

+ Training white-spaces, useless open, prlist copies random erasure.
Too many "open Errors" on the contrary.

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

6 files changed, 21 insertions, 21 deletions

diff --git a/plugins/xml/acic2Xml.ml4 b/plugins/xml/acic2Xml.ml4
index 97f7e2bd4..75bc84074 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
-    [] -> Util.anomaly "find_last_id: empty list"
+    [] -> Errors.anomaly "find_last_id: empty list"
   | [id,_,_] -> id
   | _::tl -> find_last_id tl
 ;;
diff --git a/plugins/xml/cic2acic.ml b/plugins/xml/cic2acic.ml
index da0a65ff5..78a402898 100644
--- a/plugins/xml/cic2acic.ml
+++ b/plugins/xml/cic2acic.ml
@@ -59,7 +59,7 @@ let get_uri_of_var v pvars =
  let module N = Names in
   let rec search_in_open_sections =
    function
-      [] -> Util.error ("Variable "^v^" not found")
+      [] -> Errors.error ("Variable "^v^" not found")
     | he::tl as modules ->
        let dirpath = N.make_dirpath modules in
         if List.mem (N.id_of_string v) (D.last_section_hyps dirpath) then
@@ -162,7 +162,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 *)
-  | _ -> Util.anomaly "family_of_term"
+  | _ -> Errors.anomaly "family_of_term"
 ;;
 
 module CPropRetyping =
@@ -177,7 +177,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
-        | _ -> Util.anomaly "Non-functional construction"
+        | _ -> Errors.anomaly "Non-functional construction"
 
 
   let sort_of_atomic_type env sigma ft args =
@@ -193,7 +193,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 -> Util.anomaly "type_of: this is not a well-typed term")
+           with Not_found -> Errors.anomaly "type_of: this is not a well-typed term")
     | T.Rel n ->
         let (_,_,ty) = Environ.lookup_rel n env in
         T.lift n ty
@@ -202,7 +202,7 @@ let typeur sigma metamap =
           let (_,_,ty) = Environ.lookup_named id env in
           ty
         with Not_found ->
-          Util.anomaly ("type_of: variable "^(Names.string_of_id id)^" unbound"))
+          Errors.anomaly ("type_of: variable "^(Names.string_of_id id)^" unbound"))
     | T.Const c ->
         let cb = Environ.lookup_constant c env in
         Typeops.type_of_constant_type env (cb.Declarations.const_type)
@@ -212,7 +212,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 -> Util.anomaly "type_of: Bad recursive type" in
+          with Not_found -> Errors.anomaly "type_of: 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 +253,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 _ ->
-        Util.anomaly "sort_of: Not a type (1)"
+        Errors.anomaly "sort_of: Not a type (1)"
     | _ -> outsort env sigma (type_of env t)
 
   and sort_family_of env t =
@@ -265,7 +265,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 _ ->
-        Util.anomaly "sort_of: Not a type (1)"
+        Errors.anomaly "sort_of: Not a type (1)"
     | _ -> outsort env sigma (type_of env t)
 
   in type_of, sort_of, sort_family_of
@@ -523,7 +523,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 _ -> Util.anomaly "Meta met during exporting to XML"
+           | T.Meta _ -> Errors.anomaly "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 ;
@@ -737,7 +737,7 @@ print_endline "PASSATO" ; flush stdout ;
                 let ids = ref (Termops.ids_of_context env) in
                  Array.map
                   (function
-                      N.Anonymous -> Util.error "Anonymous fix function met"
+                      N.Anonymous -> Errors.error "Anonymous fix function met"
                     | N.Name id as n ->
                        let res = N.Name (Namegen.next_name_away n !ids) in
                         ids := id::!ids ;
@@ -750,7 +750,7 @@ print_endline "PASSATO" ; flush stdout ;
                     let fi' =
                      match fi with
                         N.Name fi -> fi
-                      | N.Anonymous -> Util.error "Anonymous fix function met"
+                      | N.Anonymous -> Errors.error "Anonymous fix function met"
                     in
                      (id, fi', ai,
                       aux' env idrefs ti,
@@ -771,7 +771,7 @@ print_endline "PASSATO" ; flush stdout ;
                 let ids = ref (Termops.ids_of_context env) in
                  Array.map
                   (function
-                      N.Anonymous -> Util.error "Anonymous fix function met"
+                      N.Anonymous -> Errors.error "Anonymous fix function met"
                     | N.Name id as n ->
                        let res = N.Name (Namegen.next_name_away n !ids) in
                         ids := id::!ids ;
@@ -784,7 +784,7 @@ print_endline "PASSATO" ; flush stdout ;
                     let fi' =
                      match fi with
                         N.Name fi -> fi
-                      | N.Anonymous -> Util.error "Anonymous fix function met"
+                      | N.Anonymous -> Errors.error "Anonymous fix function met"
                     in
                      (id, fi',
                       aux' env idrefs ti,
diff --git a/plugins/xml/doubleTypeInference.ml b/plugins/xml/doubleTypeInference.ml
index a21a919ad..30cd5c18b 100644
--- a/plugins/xml/doubleTypeInference.ml
+++ b/plugins/xml/doubleTypeInference.ml
@@ -67,7 +67,7 @@ let double_type_of env sigma cstr expectedty subterms_to_types =
    let judgement =
     match T.kind_of_term cstr with
        T.Meta n ->
-        Util.error
+        Errors.error
          "DoubleTypeInference.double_type_of: found a non-instanciated goal"
 
      | T.Evar ((n,l) as ev) ->
diff --git a/plugins/xml/dumptree.ml4 b/plugins/xml/dumptree.ml4
index 3c3e54fa3..69b9e6ea7 100644
--- a/plugins/xml/dumptree.ml4
+++ b/plugins/xml/dumptree.ml4
@@ -128,7 +128,7 @@ let pr_goal_xml sigma g =
 ;;
 
 let print_proof_xml () =
-  Util.anomaly "Dump Tree command not supported in this version."
+  Errors.anomaly "Dump Tree command not supported in this version."
 
 
 VERNAC COMMAND EXTEND DumpTree
diff --git a/plugins/xml/proofTree2Xml.ml4 b/plugins/xml/proofTree2Xml.ml4
index 2f5eb6ac2..21058a7b9 100644
--- a/plugins/xml/proofTree2Xml.ml4
+++ b/plugins/xml/proofTree2Xml.ml4
@@ -53,7 +53,7 @@ let constr_to_xml obj sigma env =
     in
      Acic2Xml.print_term ids_to_inner_sorts annobj
    with e ->
-    Util.anomaly
+    Errors.anomaly
      ("Problem during the conversion of constr into XML: " ^
       Printexc.to_string e)
 (* CSC: debugging stuff
diff --git a/plugins/xml/xmlcommand.ml b/plugins/xml/xmlcommand.ml
index 1037bbf08..13821488a 100644
--- a/plugins/xml/xmlcommand.ml
+++ b/plugins/xml/xmlcommand.ml
@@ -424,7 +424,7 @@ let kind_of_variable id =
     | DK.IsAssumption DK.Conjectural -> "VARIABLE","Conjecture"
     | DK.IsDefinition DK.Definition -> "VARIABLE","LocalDefinition"
     | DK.IsProof _ -> "VARIABLE","LocalFact"
-    | _ -> Util.anomaly "Unsupported variable kind"
+    | _ -> Errors.anomaly "Unsupported variable kind"
 ;;
 
 let kind_of_constant kn =
@@ -541,7 +541,7 @@ let print internal glob_ref kind xml_library_root =
             D.mind_finite=finite} = mib in
           Cic2acic.Inductive kn,mk_inductive_obj kn mib packs variables nparams hyps finite
     | Ln.ConstructRef _ ->
-       Util.error ("a single constructor cannot be printed in XML")
+       Errors.error ("a single constructor cannot be printed in XML")
   in
   let fn = filename_of_path xml_library_root tag in
   let uri = Cic2acic.uri_of_kernel_name tag in
@@ -560,7 +560,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
-   Util.anomaly "Xmlcommand.show_pftreestate is not supported in this version."
+   Errors.anomaly "Xmlcommand.show_pftreestate is not supported in this version."
 
 let show fn =
  let pftst = Pfedit.get_pftreestate () in
@@ -656,7 +656,7 @@ let _ =
 	  let options = " --html -s --body-only --no-index --latin1 --raw-comments" in
           let command cmd =
            if Sys.command cmd <> 0 then
-            Util.anomaly ("Error executing \"" ^ cmd ^ "\"")
+            Errors.anomaly ("Error executing \"" ^ cmd ^ "\"")
           in
            command (coqdoc^options^" -o "^fn^".xml "^fn^".v");
            command ("rm "^fn^".v "^fn^".glob");