diff options
| author | Hugo Herbelin | 2014-07-01 10:53:26 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2014-07-01 11:55:03 +0200 |
| commit | f8e74d5baa18513fb8f697aaa7e8a495c9a2a9d5 (patch) | |
| tree | 9024ff3277016995cf3e03a6ffd8f3b3316e677f | |
| 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.
| -rw-r--r-- | tactics/tacinterp.ml | 2 | ||||
| -rw-r--r-- | toplevel/cerrors.ml | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index cd38f6768f..06ec278cc3 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -708,7 +708,7 @@ let interp_message_nl ist gl = function let interp_message ist gl l = (* Force evaluation of interp_message_token so that potential errors are raised now and not at printing time *) - prlist (fun x -> spc () ++ x) (List.map (interp_message_token ist gl) l) + prlist_with_sep spc (interp_message_token ist gl) l let rec interp_intro_pattern ist env = function | loc, IntroOrAndPattern l -> diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml index f5cc2015b8..9c15b20686 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 ".") |