diff options
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/cerrors.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml index f5cc2015b..9c15b2068 100644 --- a/toplevel/cerrors.ml +++ b/toplevel/cerrors.ml @@ -94,7 +94,7 @@ let process_vernac_interp_error exn = match exn with let s = Lazy.force s in wrap_vernac_error exn (str "Tactic failure" ++ - (if Pp.is_empty s then s else str ":" ++ s) ++ + (if Pp.is_empty s then s else str ": " ++ s) ++ if Int.equal i 0 then str "." else str " (level " ++ int i ++ str").") | AlreadyDeclared msg -> wrap_vernac_error exn (msg ++ str ".") |