From f8e74d5baa18513fb8f697aaa7e8a495c9a2a9d5 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 1 Jul 2014 10:53:26 +0200
Subject: Fixing the place where to insert a space in "Tactic failure" message.
 Otherwise, a heading space was missing when calling tclFAIL from ML tactics.

---
 tactics/tacinterp.ml | 2 +-
 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 ".")
-- 
cgit v1.2.3