From 9a48211ea8439a8502145e508b70ede9b5929b2f Mon Sep 17 00:00:00 2001 From: Gaetan Gilbert Date: Thu, 27 Apr 2017 21:58:52 +0200 Subject: Post-rebase warnings (unused opens and 2 unused values) --- vernac/topfmt.ml | 1 - 1 file changed, 1 deletion(-) (limited to 'vernac/topfmt.ml') diff --git a/vernac/topfmt.ml b/vernac/topfmt.ml index e44b585d7..6d9d71a62 100644 --- a/vernac/topfmt.ml +++ b/vernac/topfmt.ml @@ -131,7 +131,6 @@ 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 ?pre_hdr s = pr_opt_no_spc (fun x -> x ++ fnl ()) pre_hdr ++ quoter (hov 0 (info ++ s)) -- cgit v1.2.3