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 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'tactics/tacinterp.ml') diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index cd38f6768..06ec278cc 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 -> -- cgit v1.2.3