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.

---
 toplevel/cerrors.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'toplevel')

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