From 24879dc0e59856e297b0172d00d67df67fbb0184 Mon Sep 17 00:00:00 2001 From: ppedrot Date: Wed, 30 May 2012 16:05:13 +0000 Subject: More uniformisation in Pp.warn functions. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15399 85f007b7-540e-0410-9357-904b9bb8a0f7 --- checker/checker.ml | 4 ++-- interp/topconstr.ml | 2 +- kernel/univ.ml | 2 +- lib/pp.ml4 | 1 - lib/pp.mli | 2 -- library/library.ml | 2 +- plugins/xml/cic2acic.ml | 4 ++-- plugins/xml/xmlcommand.ml | 26 +++++++++++++------------- pretyping/detyping.ml | 2 +- printing/printer.ml | 4 ++-- tactics/auto.ml | 2 +- tactics/tacinterp.ml | 4 ++-- toplevel/class.ml | 2 +- toplevel/command.ml | 2 +- toplevel/coqtop.ml | 4 ++-- toplevel/indschemes.ml | 2 +- toplevel/metasyntax.ml | 4 ++-- toplevel/mltop.ml4 | 2 +- toplevel/obligations.ml | 2 -- toplevel/vernacentries.ml | 2 +- 20 files changed, 35 insertions(+), 40 deletions(-) diff --git a/checker/checker.ml b/checker/checker.ml index 44a77836c..7ea55d833 100644 --- a/checker/checker.ml +++ b/checker/checker.ml @@ -68,8 +68,8 @@ let add_path ~unix_path:dir ~coq_root:coq_dirpath = let convert_string d = try id_of_string d with _ -> - if_verbose warning - ("Directory "^d^" cannot be used as a Coq identifier (skipped)"); + if_verbose msg_warning + (str ("Directory "^d^" cannot be used as a Coq identifier (skipped)")); flush_all (); failwith "caught" diff --git a/interp/topconstr.ml b/interp/topconstr.ml index 824b7f59a..1036baf7c 100644 --- a/interp/topconstr.ml +++ b/interp/topconstr.ml @@ -138,7 +138,7 @@ let fold_constr_expr_with_binders g f n acc = function fold_local_binders g f n' (fold_local_binders g f n acc t lb) c lb) l acc | CCoFix (loc,_,_) -> - Pp.warning "Capture check in multiple binders not done"; acc + msg_warning (str "Capture check in multiple binders not done"); acc let free_vars_of_constr_expr c = let rec aux bdvars l = function diff --git a/kernel/univ.ml b/kernel/univ.ml index a6942ea88..2384fdd55 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -172,7 +172,7 @@ let type0_univ = Atom UniverseLevel.Set let is_type0_univ = function | Atom UniverseLevel.Set -> true - | Max ([UniverseLevel.Set], []) -> warning "Non canonical Set"; true + | Max ([UniverseLevel.Set], []) -> msg_warning (str "Non canonical Set"); true | u -> false let is_univ_variable = function diff --git a/lib/pp.ml4 b/lib/pp.ml4 index ff1973846..0a3466859 100644 --- a/lib/pp.ml4 +++ b/lib/pp.ml4 @@ -321,7 +321,6 @@ let pperr x = pp_with !err_ft x let pperrnl x = ppnl_with !err_ft x let message s = ppnl (str s) let warning x = warning_with !err_ft x -let warn x = warn_with !err_ft x let pp_flush x = Format.pp_print_flush !std_ft x let flush_all() = flush stderr; flush stdout; pp_flush() diff --git a/lib/pp.mli b/lib/pp.mli index 112d97655..da37a1153 100644 --- a/lib/pp.mli +++ b/lib/pp.mli @@ -101,8 +101,6 @@ val ppnl : std_ppcmds -> unit val pperr : std_ppcmds -> unit val pperrnl : std_ppcmds -> unit val message : string -> unit (** = pPNL *) -val warning : string -> unit -val warn : std_ppcmds -> unit val pp_flush : unit -> unit val flush_all: unit -> unit diff --git a/library/library.ml b/library/library.ml index 66bca4f1b..417c567a8 100644 --- a/library/library.ml +++ b/library/library.ml @@ -656,7 +656,7 @@ let save_library_to dir f = System.marshal_out ch di; System.marshal_out ch table; close_out ch - with e -> warning ("Removed file "^f'); close_out ch; Sys.remove f'; raise e + with e -> msg_warning (str ("Removed file "^f')); close_out ch; Sys.remove f'; raise e (************************************************************************) (*s Display the memory use of a library. *) diff --git a/plugins/xml/cic2acic.ml b/plugins/xml/cic2acic.ml index ec0910d7f..e29fcd0e8 100644 --- a/plugins/xml/cic2acic.ml +++ b/plugins/xml/cic2acic.ml @@ -23,8 +23,8 @@ let get_module_path_of_full_path path = (function modul -> Libnames.is_dirpath_prefix_of modul dirpath) modules with [] -> - Pp.warning ("Modules not supported: reference to "^ - Libnames.string_of_path path^" will be wrong"); + Pp.msg_warning (Pp.str ("Modules not supported: reference to "^ + Libnames.string_of_path path^" will be wrong")); dirpath | [modul] -> modul | _ -> diff --git a/plugins/xml/xmlcommand.ml b/plugins/xml/xmlcommand.ml index 81dba546e..ee9bcb25d 100644 --- a/plugins/xml/xmlcommand.ml +++ b/plugins/xml/xmlcommand.ml @@ -426,46 +426,46 @@ let kind_of_constant kn = | IsAssumption Definitional -> "AXIOM","Declaration" | IsAssumption Logical -> "AXIOM","Axiom" | IsAssumption Conjectural -> - Pp.warning "Conjecture not supported in dtd (used Declaration instead)"; + Pp.msg_warning (Pp.str "Conjecture not supported in dtd (used Declaration instead)"); "AXIOM","Declaration" | IsDefinition Definition -> "DEFINITION","Definition" | IsDefinition Example -> - Pp.warning "Example not supported in dtd (used Definition instead)"; + Pp.msg_warning (Pp.str "Example not supported in dtd (used Definition instead)"); "DEFINITION","Definition" | IsDefinition Coercion -> - Pp.warning "Coercion not supported in dtd (used Definition instead)"; + Pp.msg_warning (Pp.str "Coercion not supported in dtd (used Definition instead)"); "DEFINITION","Definition" | IsDefinition SubClass -> - Pp.warning "SubClass not supported in dtd (used Definition instead)"; + Pp.msg_warning (Pp.str "SubClass not supported in dtd (used Definition instead)"); "DEFINITION","Definition" | IsDefinition CanonicalStructure -> - Pp.warning "CanonicalStructure not supported in dtd (used Definition instead)"; + Pp.msg_warning (Pp.str "CanonicalStructure not supported in dtd (used Definition instead)"); "DEFINITION","Definition" | IsDefinition Fixpoint -> - Pp.warning "Fixpoint not supported in dtd (used Definition instead)"; + Pp.msg_warning (Pp.str "Fixpoint not supported in dtd (used Definition instead)"); "DEFINITION","Definition" | IsDefinition CoFixpoint -> - Pp.warning "CoFixpoint not supported in dtd (used Definition instead)"; + Pp.msg_warning (Pp.str "CoFixpoint not supported in dtd (used Definition instead)"); "DEFINITION","Definition" | IsDefinition Scheme -> - Pp.warning "Scheme not supported in dtd (used Definition instead)"; + Pp.msg_warning (Pp.str "Scheme not supported in dtd (used Definition instead)"); "DEFINITION","Definition" | IsDefinition StructureComponent -> - Pp.warning "StructureComponent not supported in dtd (used Definition instead)"; + Pp.msg_warning (Pp.str "StructureComponent not supported in dtd (used Definition instead)"); "DEFINITION","Definition" | IsDefinition IdentityCoercion -> - Pp.warning "IdentityCoercion not supported in dtd (used Definition instead)"; + Pp.msg_warning (Pp.str "IdentityCoercion not supported in dtd (used Definition instead)"); "DEFINITION","Definition" | IsDefinition Instance -> - Pp.warning "Instance not supported in dtd (used Definition instead)"; + Pp.msg_warning (Pp.str "Instance not supported in dtd (used Definition instead)"); "DEFINITION","Definition" | IsDefinition Method -> - Pp.warning "Method not supported in dtd (used Definition instead)"; + Pp.msg_warning (Pp.str "Method not supported in dtd (used Definition instead)"); "DEFINITION","Definition" | IsProof (Theorem|Lemma|Corollary|Fact|Remark as thm) -> "THEOREM",Kindops.string_of_theorem_kind thm | IsProof _ -> - Pp.warning "Unsupported theorem kind (used Theorem instead)"; + Pp.msg_warning (Pp.str "Unsupported theorem kind (used Theorem instead)"); "THEOREM",Kindops.string_of_theorem_kind Theorem ;; diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index fd20f199c..a3fe0d059 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -490,7 +490,7 @@ and share_names isgoal n l avoid env c t = share_names isgoal (n-1) ((Name id,Explicit,None,t')::l) avoid env appc c' (* If built with the f/n notation: we renounce to share names *) | _ -> - if n>0 then warning "Detyping.detype: cannot factorize fix enough"; + if n>0 then msg_warning (str "Detyping.detype: cannot factorize fix enough"); let c = detype isgoal avoid env c in let t = detype isgoal avoid env t in (List.rev l,c,t) diff --git a/printing/printer.ml b/printing/printer.ml index 1c51a6755..54e78a716 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -480,7 +480,7 @@ let pr_prim_rule = function (str"fix " ++ pr_id f ++ str"/" ++ int n) | FixRule (f,n,others,j) -> - if j<>0 then warning "Unsupported printing of \"fix\""; + if j<>0 then msg_warning (str "Unsupported printing of \"fix\""); let rec print_mut = function | (f,n,ar)::oth -> pr_id f ++ str"/" ++ int n ++ str" : " ++ pr_lconstr ar ++ print_mut oth @@ -492,7 +492,7 @@ let pr_prim_rule = function (str"cofix " ++ pr_id f) | Cofix (f,others,j) -> - if j<>0 then warning "Unsupported printing of \"fix\""; + if j<>0 then msg_warning (str "Unsupported printing of \"fix\""); let rec print_mut = function | (f,ar)::oth -> (pr_id f ++ str" : " ++ pr_lconstr ar ++ print_mut oth) diff --git a/tactics/auto.ml b/tactics/auto.ml index 6146998cb..404516279 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -518,7 +518,7 @@ let make_apply_entry env sigma (eapply,hnf,verbose) pri ?(name=PathAny) (c,cty) else begin if not eapply then failwith "make_apply_entry"; if verbose then - warn (str "the hint: eapply " ++ pr_lconstr c ++ + msg_warning (str "the hint: eapply " ++ pr_lconstr c ++ str " will only be used by eauto"); (Some hd, { pri = (match pri with None -> nb_hyp cty + nmiss | Some p -> p); diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index d98167ed0..0bcc4ed47 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -235,7 +235,7 @@ let add_tactic s t = let overwriting_add_tactic s t = if Hashtbl.mem tac_tab s then begin Hashtbl.remove tac_tab s; - warning ("Overwriting definition of tactic "^s) + msg_warning (str ("Overwriting definition of tactic "^s)) end; Hashtbl.add tac_tab s t @@ -273,7 +273,7 @@ let lookup_genarg id = try Gmap.find id !extragenargtab with Not_found -> let msg = "No interpretation function found for entry " ^ id in - warning msg; + msg_warning (str msg); let f = (fun _ _ -> failwith msg), (fun _ _ _ -> failwith msg), (fun _ a -> a) in add_interp_genarg id f; f diff --git a/toplevel/class.ml b/toplevel/class.ml index 4c267ca83..ad2eb69b4 100644 --- a/toplevel/class.ml +++ b/toplevel/class.ml @@ -261,7 +261,7 @@ let add_new_coercion_core coef stre source target isid = in check_source (Some cls); if not (uniform_cond (llp-ind) lvs) then - warning (Pp.string_of_ppcmds (explain_coercion_error coef NotUniform)); + msg_warning (explain_coercion_error coef NotUniform); let clt = try get_target tg ind diff --git a/toplevel/command.ml b/toplevel/command.ml index 51d66a761..12ce73a5b 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -91,7 +91,7 @@ let interp_definition bl red_option c ctypopt = let typ = nf_evar !evdref (it_mkProd_or_LetIn ty ctx) in (* Check that all implicit arguments inferable from the term is inferable from the type *) if not (try List.for_all (fun (key,va) -> List.assoc key impsty = va) imps2 with Not_found -> false) - then warn (str "Implicit arguments declaration relies on type." ++ + then msg_warning (str "Implicit arguments declaration relies on type." ++ spc () ++ str "The term declares more implicits than the type here."); imps1@(Impargs.lift_implicits nb_args impsty), { const_entry_body = body; diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 3936d2e80..2bc4fa97c 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -123,8 +123,8 @@ let compile_files () = let set_compat_version = function | "8.3" -> compat_version := Some V8_3 | "8.2" -> compat_version := Some V8_2 - | "8.1" -> warning "Compatibility with version 8.1 not supported." - | "8.0" -> warning "Compatibility with version 8.0 not supported." + | "8.1" -> msg_warning (str "Compatibility with version 8.1 not supported.") + | "8.0" -> msg_warning (str "Compatibility with version 8.0 not supported.") | s -> error ("Unknown compatibility version \""^s^"\".") (*s options for the virtual machine *) diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml index 3fba117a9..8804c60c8 100644 --- a/toplevel/indschemes.ml +++ b/toplevel/indschemes.ml @@ -272,7 +272,7 @@ let declare_congr_scheme ind = then ignore (define_individual_scheme congr_scheme_kind KernelVerbose None ind) else - warning "Cannot build congruence scheme because eq is not found" + msg_warning (str "Cannot build congruence scheme because eq is not found") end let declare_sym_scheme ind = diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index e98aa8c26..fe7394e94 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -846,7 +846,7 @@ let check_rule_productivity l = error "A recursive notation must start with at least one symbol." let is_not_printable = function - | NVar _ -> warning "This notation will not be used for printing as it is bound to a \nsingle variable"; true + | NVar _ -> msg_warning (str "This notation will not be used for printing as it is bound to a single variable."); true | _ -> false let find_precedence lev etyps symbols = @@ -904,7 +904,7 @@ let remove_curly_brackets l = (match next' with | Terminal "}" as t2 :: l'' as l1 -> if l <> l0 or l' <> l1 then - warning "Skipping spaces inside curly brackets"; + msg_warning (str "Skipping spaces inside curly brackets"); if deb & l'' = [] then [t1;x;t2] else begin check_curly_brackets_notation_exists (); x :: aux false l'' diff --git a/toplevel/mltop.ml4 b/toplevel/mltop.ml4 index e02e6329d..2256d1b1d 100644 --- a/toplevel/mltop.ml4 +++ b/toplevel/mltop.ml4 @@ -117,7 +117,7 @@ let dir_ml_load s = let dir_ml_use s = match !load with | WithTop t -> t.use_file s - | _ -> warning "Cannot access the ML compiler" + | _ -> msg_warning (str "Cannot access the ML compiler") (* Adds a path to the ML paths *) let add_ml_dir s = diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml index 5ca9ac9b4..61cc6b348 100644 --- a/toplevel/obligations.ml +++ b/toplevel/obligations.ml @@ -300,7 +300,6 @@ let safe_init_constant md name () = let fix_proto = safe_init_constant tactics_module "fix_proto" let hide_obligation = safe_init_constant tactics_module "obligation" -let ppwarn cmd = Pp.warn (str"Program:" ++ cmd) let pperror cmd = Errors.errorlabstrm "Program" cmd let error s = pperror (str s) @@ -736,7 +735,6 @@ let not_transp_msg = str "Obligation should be transparent but was declared opaque." ++ spc () ++ str"Use 'Defined' instead." -let warn_not_transp () = ppwarn not_transp_msg let error_not_transp () = pperror not_transp_msg let rec string_of_list sep f = function diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 2d3886a1d..dd8f1cd0e 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -739,7 +739,7 @@ let vernac_chdir = function | Some path -> begin try Sys.chdir (Envars.expand_path_macros ~warn:(fun x -> msg_warning (str x)) path) - with Sys_error str -> warning ("Cd failed: " ^ str) + with Sys_error err -> msg_warning (str ("Cd failed: " ^ err)) end; if_verbose message (Sys.getcwd()) -- cgit v1.2.3