aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac/explainErr.ml
diff options
context:
space:
mode:
Diffstat (limited to 'vernac/explainErr.ml')
-rw-r--r--vernac/explainErr.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/explainErr.ml b/vernac/explainErr.ml
index 17897460c..148d029bc 100644
--- a/vernac/explainErr.ml
+++ b/vernac/explainErr.ml
@@ -47,7 +47,7 @@ let _ = CErrors.register_handler explain_exn_default
let wrap_vernac_error with_header (exn, info) strm =
if with_header then
- let header = Pp.tag (Pp.Tag.inj Ppstyle.error_tag Ppstyle.tag) (str "Error:") in
+ let header = Pp.tag Ppstyle.error_tag (str "Error:") in
let e = EvaluatedError (hov 0 (header ++ spc () ++ strm), None) in
(e, info)
else