diff options
Diffstat (limited to 'vernac/topfmt.ml')
| -rw-r--r-- | vernac/topfmt.ml | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/vernac/topfmt.ml b/vernac/topfmt.ml index 6d9d71a62..bbf2ed4fc 100644 --- a/vernac/topfmt.ml +++ b/vernac/topfmt.ml @@ -260,8 +260,6 @@ let emacs_logger = gen_logger Emacs.quote_info Emacs.quote_warning (* This is specific to the toplevel *) let pr_loc loc = - if Loc.is_ghost loc then str"<unknown>" - else let fname = loc.Loc.fname in if CString.equal fname "" then Loc.(str"Toplevel input, characters " ++ int loc.bp ++ @@ -275,7 +273,7 @@ let pr_loc loc = let print_err_exn ?extra any = let (e, info) = CErrors.push any in let loc = Loc.get_loc info in - let msg_loc = pr_loc (Option.default Loc.ghost loc) in + let msg_loc = Option.cata pr_loc (mt ()) loc in let pre_hdr = pr_opt_no_spc (fun x -> x) extra ++ msg_loc in let msg = CErrors.iprint (e, info) ++ fnl () in std_logger ~pre_hdr Feedback.Error msg |