From 401f17afa2e9cc3f2d734aef0d71a2c363838ebd Mon Sep 17 00:00:00 2001 From: pboutill Date: Fri, 2 Mar 2012 22:30:29 +0000 Subject: 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 --- plugins/xml/acic2Xml.ml4 | 2 +- plugins/xml/cic2acic.ml | 26 +++++++++++++------------- plugins/xml/doubleTypeInference.ml | 2 +- plugins/xml/dumptree.ml4 | 2 +- plugins/xml/proofTree2Xml.ml4 | 2 +- plugins/xml/xmlcommand.ml | 8 ++++---- 6 files changed, 21 insertions(+), 21 deletions(-) (limited to 'plugins/xml') 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"); -- cgit v1.2.3