diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-03-22 23:23:14 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-03-24 13:14:59 +0100 |
| commit | 43ac25fd5218fb92b3971c8df8be4f38894e27f3 (patch) | |
| tree | 03f1da9560f09a0c04d4c2823ae30b8459988556 | |
| parent | 530cd175c1b7465c3fa35c300f42b022bed9b25b (diff) | |
[nit] Fix a couple incorrect uses of msg_error.
| -rw-r--r-- | library/summary.ml | 2 | ||||
| -rw-r--r-- | proofs/proof_using.ml | 2 | ||||
| -rw-r--r-- | toplevel/vernac.ml | 6 | ||||
| -rw-r--r-- | 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. *) |