diff options
Diffstat (limited to 'ltac/tacinterp.ml')
| -rw-r--r-- | ltac/tacinterp.ml | 11 |
1 files changed, 7 insertions, 4 deletions
diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml index e814cc7e6..9a4beed87 100644 --- a/ltac/tacinterp.ml +++ b/ltac/tacinterp.ml @@ -1144,6 +1144,12 @@ let rec read_match_rule lfun ist env sigma = function :: read_match_rule lfun ist env sigma tl | [] -> [] +let warn_deprecated_info = + CWarnings.create ~name:"deprecated-info-tactical" ~category:"deprecated" + (fun () -> + 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.") (* Interprets an l-tac expression into a value *) let rec val_interp ist ?(appl=UnnamedAppl) (tac:glob_tactic_expr) : Val.t Ftactic.t = @@ -1251,10 +1257,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 -> - 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."); + warn_deprecated_info (); eval_tactic ist tac | TacSelect (sel, tac) -> Tacticals.New.tclSELECT sel (interp_tactic ist tac) (* For extensions *) |