diff options
| -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 ".") |