From 14155762a7cd46ed6a3e9cf2a58e11ee1244b188 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 1 Jun 2016 18:31:05 +0200 Subject: [pp] Replace `Pp.Tag` by `Ppstyle.tag` = `string list` This is what has always been used, so it doesn't represent a functional change. This is just a preliminary patch, but many more possibilities could be done wrt tags. --- vernac/explainErr.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'vernac/explainErr.ml') 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 -- cgit v1.2.3