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/xmlcommand.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'plugins/xml/xmlcommand.ml') 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