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