diff options
Diffstat (limited to 'ltac/tacenv.ml')
| -rw-r--r-- | ltac/tacenv.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/ltac/tacenv.ml b/ltac/tacenv.ml index 39db6268b..005d1f5f4 100644 --- a/ltac/tacenv.ml +++ b/ltac/tacenv.ml @@ -54,7 +54,7 @@ let register_ml_tactic ?(overwrite = false) s (t : ml_tactic array) = if MLTacMap.mem s !tac_tab then if overwrite then let () = tac_tab := MLTacMap.remove s !tac_tab in - msg_warning (str "Overwriting definition of tactic " ++ pr_tacname s) + Feedback.msg_warning (str "Overwriting definition of tactic " ++ pr_tacname s) else Errors.anomaly (str "Cannot redeclare tactic " ++ pr_tacname s ++ str ".") in |