aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--toplevel/vernac.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index d4146ace1..92730c14d 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -111,7 +111,7 @@ let pr_open_cur_subgoals () =
with Proof_global.NoCurrentProof -> Pp.str ""
let vernac_error msg =
- Format.fprintf !Topfmt.err_ft "@[%a@]%!" Pp.pp_with msg;
+ Topfmt.std_logger Feedback.Error msg;
flush_all ();
exit 1