aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/vernac.ml
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel/vernac.ml')
-rw-r--r--toplevel/vernac.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 74adf497e..0f3a90c3e 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -143,7 +143,7 @@ let pr_new_syntax_in_context loc chan_beautify ocom =
| None -> mt() in
let after = comment (CLexer.extract_comments (snd loc)) in
if !beautify_file then
- Pp.msg_with !Pp_control.std_ft (hov 0 (before ++ com ++ after))
+ Pp.msg_with ~pp_tag:Ppstyle.pp_tag !Pp_control.std_ft (hov 0 (before ++ com ++ after))
else
Feedback.msg_info (hov 4 (str"New Syntax:" ++ fnl() ++ (hov 0 com)));
States.unfreeze fs;
@@ -181,7 +181,7 @@ let pp_cmd_header loc com =
and take control of the console.
*)
let print_cmd_header loc com =
- Pp.pp_with !Pp_control.std_ft (pp_cmd_header loc com);
+ Pp.pp_with ~pp_tag:Ppstyle.pp_tag !Pp_control.std_ft (pp_cmd_header loc com);
Format.pp_print_flush !Pp_control.std_ft ()
let rec interp_vernac po chan_beautify checknav (loc,com) =