diff options
Diffstat (limited to 'grammar')
| -rw-r--r-- | grammar/tacextend.mlp | 4 | ||||
| -rw-r--r-- | grammar/vernacextend.mlp | 2 |
2 files changed, 3 insertions, 3 deletions
diff --git a/grammar/tacextend.mlp b/grammar/tacextend.mlp index 1d52a85a5..ac6a7ac7f 100644 --- a/grammar/tacextend.mlp +++ b/grammar/tacextend.mlp @@ -115,7 +115,7 @@ let declare_tactic loc s c cl = match cl with Tacenv.register_ml_tactic $se$ [|$tac$|]; Mltop.declare_cache_obj obj $plugin_name$; } with [ e when Errors.noncritical e -> - Pp.msg_warning + Feedback.msg_warning (Pp.app (Pp.str ("Exception in tactic extend " ^ $entry$ ^": ")) (Errors.print e)) ]; } >> @@ -133,7 +133,7 @@ let declare_tactic loc s c cl = match cl with Tacenv.register_ml_tactic $se$ (Array.of_list $make_fun_clauses loc s cl$); Mltop.declare_cache_obj $obj$ $plugin_name$; } with [ e when Errors.noncritical e -> - Pp.msg_warning + Feedback.msg_warning (Pp.app (Pp.str ("Exception in tactic extend " ^ $entry$ ^": ")) (Errors.print e)) ]; } >> diff --git a/grammar/vernacextend.mlp b/grammar/vernacextend.mlp index fa8610fb9..ce0431889 100644 --- a/grammar/vernacextend.mlp +++ b/grammar/vernacextend.mlp @@ -126,7 +126,7 @@ let declare_command loc s c nt cl = CList.iteri (fun i (depr, f) -> Vernacinterp.vinterp_add depr ($se$, i) f) $funcl$; CList.iteri (fun i f -> Vernac_classifier.declare_vernac_classifier ($se$, i) f) $classl$ } with [ e when Errors.noncritical e -> - Pp.msg_warning + Feedback.msg_warning (Pp.app (Pp.str ("Exception in vernac extend " ^ $se$ ^": ")) (Errors.print e)) ]; |