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 /tactics | |
| 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 'tactics')
| -rw-r--r-- | tactics/tacinterp.ml | 2 |
1 files changed, 1 insertions, 1 deletions
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 -> |