diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-07-01 10:53:26 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-07-01 11:55:03 +0200 |
| commit | f8e74d5baa18513fb8f697aaa7e8a495c9a2a9d5 (patch) | |
| tree | 9024ff3277016995cf3e03a6ffd8f3b3316e677f /toplevel | |
| parent | d755f77f9cc4760c403e588aea085733cd1f2979 (diff) | |
Fixing the place where to insert a space in "Tactic failure"
message. Otherwise, a heading space was missing when calling tclFAIL
from ML tactics.
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 ".") |