diff options
| author | Maxime Dénès | 2016-10-28 12:42:10 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2016-10-28 12:42:10 +0200 |
| commit | 3e98d3e4941f5098d743dffa8a032fd623a6a030 (patch) | |
| tree | ddfebc530ee37fce10f0cd6782c4504d9c20d486 /toplevel | |
| parent | 40dbf1e0d8824fba357632addcdce434edc8b247 (diff) | |
| parent | cb5f55380875bb3029b051eb3acfbb912d83454b (diff) | |
Merge remote-tracking branch 'github/pr/319' into v8.6
Was PR#319: More error tagging, try to fix bug 5135
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/coqloop.ml | 2 | ||||
| -rw-r--r-- | toplevel/vernac.ml | 4 |
2 files changed, 3 insertions, 3 deletions
diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml index f0f8f18641..e9771cfa40 100644 --- a/toplevel/coqloop.ml +++ b/toplevel/coqloop.ml @@ -13,7 +13,7 @@ open Flags open Vernac open Pcoq -let top_stderr x = msg_with !Pp_control.err_ft x +let top_stderr x = msg_with ~pp_tag:Ppstyle.pp_tag !Pp_control.err_ft x (* A buffer for the character read from a channel. We store the command * entered to be able to report errors without pretty-printing. *) diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index b453dbc469..de45090bfc 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) = |