diff options
Diffstat (limited to 'ltac')
| -rw-r--r-- | ltac/g_ltac.ml4 | 7 | ||||
| -rw-r--r-- | ltac/profile_ltac.ml | 8 | ||||
| -rw-r--r-- | ltac/tacentries.ml | 12 | ||||
| -rw-r--r-- | ltac/tacenv.ml | 3 | ||||
| -rw-r--r-- | ltac/tacinterp.ml | 11 |
5 files changed, 27 insertions, 14 deletions
diff --git a/ltac/g_ltac.ml4 b/ltac/g_ltac.ml4 index 517f9e3af..b5494a7cb 100644 --- a/ltac/g_ltac.ml4 +++ b/ltac/g_ltac.ml4 @@ -72,6 +72,11 @@ let test_bracket_ident = (* Tactics grammar rules *) +let warn_deprecated_appcontext = + CWarnings.create ~name:"deprecated-appcontext" ~category:"deprecated" + (fun () -> strbrk "appcontext is deprecated and will be removed " ++ + strbrk "in a future version") + GEXTEND Gram GLOBAL: tactic tacdef_body tactic_expr binder_tactic tactic_arg tactic_mode constr_may_eval constr_eval selector toplevel_selector; @@ -232,7 +237,7 @@ GEXTEND Gram Subterm (mode, oid, pc) | IDENT "appcontext"; oid = OPT Constr.ident; "["; pc = Constr.lconstr_pattern; "]" -> - Feedback.msg_warning (strbrk "appcontext is deprecated"); + warn_deprecated_appcontext ~loc:!@loc (); Subterm (true,oid, pc) | pc = Constr.lconstr_pattern -> Term pc ] ] ; diff --git a/ltac/profile_ltac.ml b/ltac/profile_ltac.ml index 9081fd3e9..f332e1a0d 100644 --- a/ltac/profile_ltac.ml +++ b/ltac/profile_ltac.ml @@ -32,10 +32,14 @@ let is_new_call () = let b = !new_call in new_call := false; b profiling results will be off. *) let encountered_multi_success_backtracking = ref false +let warn_profile_backtracking = + CWarnings.create ~name:"profile-backtracking" ~category:"ltac" + (fun () -> strbrk "Ltac Profiler cannot yet handle backtracking \ + into multi-success tactics; profiling results may be wildly inaccurate.") + let warn_encountered_multi_success_backtracking () = if !encountered_multi_success_backtracking then - Feedback.msg_warning (str "Ltac Profiler cannot yet handle backtracking \ - into multi-success tactics; profiling results may be wildly inaccurate.") + warn_profile_backtracking () let encounter_multi_success_backtracking () = if not !encountered_multi_success_backtracking diff --git a/ltac/tacentries.ml b/ltac/tacentries.ml index f00adecf2..6b7ae21f3 100644 --- a/ltac/tacentries.ml +++ b/ltac/tacentries.ml @@ -417,6 +417,11 @@ type tacdef_kind = let is_defined_tac kn = try ignore (Tacenv.interp_ltac kn); true with Not_found -> false +let warn_unusable_identifier = + CWarnings.create ~name:"unusable-identifier" ~category:"parsing" + (fun id -> strbrk "The Ltac name" ++ spc () ++ pr_id id ++ spc () ++ + strbrk "may be unusable because of a conflict with a notation.") + let register_ltac local tacl = let map tactic_body = match tactic_body with @@ -427,17 +432,14 @@ let register_ltac local tacl = Errors.user_err_loc (loc, "", str "There is already an Ltac named " ++ id_pp ++ str".") in - let is_primitive = + let is_shadowed = try match Pcoq.parse_string Pcoq.Tactic.tactic (Id.to_string id) with | Tacexpr.TacArg _ -> false | _ -> true (* most probably TacAtom, i.e. a primitive tactic ident *) with e when Errors.noncritical e -> true (* prim tactics with args, e.g. "apply" *) in - let () = if is_primitive then - Feedback.msg_warning (str "The Ltac name " ++ id_pp ++ - str " may be unusable because of a conflict with a notation.") - in + let () = if is_shadowed then warn_unusable_identifier id in NewTac id, body | TacticRedefinition (ident, body) -> let loc = loc_of_reference ident in 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 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 *) |