diff options
Diffstat (limited to 'grammar')
| -rw-r--r-- | grammar/tacextend.ml4 | 4 | ||||
| -rw-r--r-- | grammar/vernacextend.ml4 | 2 |
2 files changed, 3 insertions, 3 deletions
diff --git a/grammar/tacextend.ml4 b/grammar/tacextend.ml4 index 4c4ecaf73..0791306c4 100644 --- a/grammar/tacextend.ml4 +++ b/grammar/tacextend.ml4 @@ -117,7 +117,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)) ]; } >> @@ -135,7 +135,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.ml4 b/grammar/vernacextend.ml4 index 904662ea1..4060af8e4 100644 --- a/grammar/vernacextend.ml4 +++ b/grammar/vernacextend.ml4 @@ -128,7 +128,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)) ]; |