aboutsummaryrefslogtreecommitdiff
path: root/toplevel
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2014-11-17 10:22:31 +0100
committerPierre-Marie Pédrot2014-11-17 10:22:31 +0100
commit659ca3902a144259ec449473e95df1b3eda1b6de (patch)
tree453864b590566eeb264792699ee24b87154dc684 /toplevel
parent364decf59c14ec8a672d3c4d46fa1939ea0e52d3 (diff)
Setting error tag on generic errors returned by Coqtop.
Diffstat (limited to 'toplevel')
-rw-r--r--toplevel/cerrors.ml3
1 files changed, 2 insertions, 1 deletions
diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml
index 09ec5ce18d..8c98c813a1 100644
--- a/toplevel/cerrors.ml
+++ b/toplevel/cerrors.ml
@@ -54,7 +54,8 @@ let _ = Errors.register_handler explain_exn_default
(** Pre-explain a vernac interpretation error *)
let wrap_vernac_error exn strm =
- let e = EvaluatedError (hov 0 (str "Error:" ++ spc () ++ strm), None) in
+ let header = Pp.tag (Pp.Tag.inj Ppstyle.error_tag Ppstyle.tag) (str "Error:") in
+ let e = EvaluatedError (hov 0 (header ++ spc () ++ strm), None) in
Exninfo.copy exn e
let process_vernac_interp_error exn = match exn with