From 43ac25fd5218fb92b3971c8df8be4f38894e27f3 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 22 Mar 2017 23:23:14 +0100 Subject: [nit] Fix a couple incorrect uses of msg_error. --- library/summary.ml | 2 +- proofs/proof_using.ml | 2 +- toplevel/vernac.ml | 6 +++--- vernac/vernacentries.ml | 3 +-- 4 files changed, 6 insertions(+), 7 deletions(-) diff --git a/library/summary.ml b/library/summary.ml index 2ec4760d6..d9f644100 100644 --- a/library/summary.ml +++ b/library/summary.ml @@ -108,7 +108,7 @@ let unfreeze_summaries fs = with e when CErrors.noncritical e -> let e = CErrors.push e in Feedback.msg_error - Pp.(seq [str "Error unfrezing summay %s\n%s\n%!"; + Pp.(seq [str "Error unfreezing summary %s\n%s\n%!"; str (name_of_summary id); CErrors.iprint e]); iraise e diff --git a/proofs/proof_using.ml b/proofs/proof_using.ml index f51586c73..2c489d6de 100644 --- a/proofs/proof_using.ml +++ b/proofs/proof_using.ml @@ -108,7 +108,7 @@ let remove_ids_and_lets env s ids = let suggest_Proof_using name env vars ids_typ context_ids = let module S = Id.Set in let open Pp in - let print x = Feedback.msg_error x in + let print x = Feedback.msg_debug x in let pr_set parens s = let wrap ppcmds = if parens && S.cardinal s > 1 then str "(" ++ ppcmds ++ str ")" diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 06908abb6..9917a49b4 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -266,9 +266,9 @@ let ensure_bname src tgt = let src, tgt = Filename.basename src, Filename.basename tgt in let src, tgt = chop_extension src, chop_extension tgt in if src <> tgt then begin - Feedback.msg_error (str "Source and target file names must coincide, directories can differ"); - Feedback.msg_error (str "Source: " ++ str src); - Feedback.msg_error (str "Target: " ++ str tgt); + Feedback.msg_error (str "Source and target file names must coincide, directories can differ" ++ fnl () ++ + str "Source: " ++ str src ++ fnl () ++ + str "Target: " ++ str tgt); flush_all (); exit 1 end diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 32e18a014..f17908400 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -67,8 +67,7 @@ let show_node () = could, possibly, be cleaned away. (Feb. 2010) *) () -let show_thesis () = - Feedback.msg_error (anomaly (Pp.str "TODO") ) +let show_thesis () = CErrors.anomaly (Pp.str "Show Thesis: TODO") let show_top_evars () = (* spiwack: new as of Feb. 2010: shows goal evars in addition to non-goal evars. *) -- cgit v1.2.3