diff options
Diffstat (limited to 'vernac/explainErr.ml')
| -rw-r--r-- | vernac/explainErr.ml | 2 |
1 files changed, 1 insertions, 1 deletions
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 ".") |