From 8f8af9e4ebf1ea1ed15f765196ef5af8a77d3c27 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 29 Sep 2016 16:06:43 +0200 Subject: [pp] Prepare for serialization, remove opaque glue. We also remove flushing operations `msg_with`, now the flushing responsibility belong to the owner of the formatter. --- 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 148d029bc..5b91af03c 100644 --- a/vernac/explainErr.ml +++ b/vernac/explainErr.ml @@ -91,7 +91,7 @@ let process_vernac_interp_error with_header exn = match fst exn with let s = Lazy.force s in wrap_vernac_error with_header exn (str "Tactic failure" ++ - (if Pp.is_empty s then s else str ": " ++ s) ++ + (if Pp.ismt s then s else str ": " ++ s) ++ if Int.equal i 0 then str "." else str " (level " ++ int i ++ str").") | AlreadyDeclared msg -> wrap_vernac_error with_header exn (msg ++ str ".") -- cgit v1.2.3