aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac/topfmt.ml
diff options
context:
space:
mode:
Diffstat (limited to 'vernac/topfmt.ml')
-rw-r--r--vernac/topfmt.ml1
1 files changed, 1 insertions, 0 deletions
diff --git a/vernac/topfmt.ml b/vernac/topfmt.ml
index f843484f7..e3c0a1709 100644
--- a/vernac/topfmt.ml
+++ b/vernac/topfmt.ml
@@ -136,6 +136,7 @@ let dbg_hdr = tag Tag.debug (str "Debug:") ++ spc ()
let info_hdr = mt ()
let warn_hdr = tag Tag.warning (str "Warning:") ++ spc ()
let err_hdr = tag Tag.error (str "Error:") ++ spc ()
+let ann_hdr = tag Tag.error (str "Anomaly:") ++ spc ()
let make_body quoter info ?loc s =
let loc = Option.cata Pp.pr_loc (Pp.mt ()) loc in