diff options
Diffstat (limited to 'ltac/tacinterp.ml')
| -rw-r--r-- | ltac/tacinterp.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml index 5d282a693..406fd41ad 100644 --- a/ltac/tacinterp.ml +++ b/ltac/tacinterp.ml @@ -1242,7 +1242,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with | TacComplete tac -> Tacticals.New.tclCOMPLETE (interp_tactic ist tac) | TacArg a -> interp_tactic ist (TacArg a) | TacInfo tac -> - msg_warning + Feedback.msg_warning (strbrk "The general \"info\" tactic is currently not working." ++ spc()++ strbrk "There is an \"Info\" command to replace it." ++fnl () ++ strbrk "Some specific verbose tactics may also exist, such as info_eauto."); |