diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-11-05 12:02:43 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-11-05 12:27:11 +0100 |
| commit | d6a18782919367006ab1cee0a5577ed9b3028682 (patch) | |
| tree | e35362f80d41dcf88f17ce1f31f66a27118ddc02 /toplevel | |
| parent | ed2ec9362c0c0010b9caaaba4dcc771878ee2b7c (diff) | |
Not using style tags when translating/beautifying a file.
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/vernac.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index de45090bf..bfdae85d5 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_tag:Ppstyle.pp_tag !Pp_control.std_ft (hov 0 (before ++ com ++ after)) + Pp.msg_with !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; |