From 0daae2bd1ab518d8fcb6d59a5616786ade94d1e5 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 22 Dec 2017 16:26:24 +0100 Subject: Deprecate implicit tactic solving. --- plugins/ltac/extratactics.ml4 | 6 ++++++ 1 file changed, 6 insertions(+) (limited to 'plugins/ltac') diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4 index c5254b37c..2a6e8c060 100644 --- a/plugins/ltac/extratactics.ml4 +++ b/plugins/ltac/extratactics.ml4 @@ -594,10 +594,16 @@ let inImplicitTactic : glob_tactic_expr option -> obj = subst_function = subst_implicit_tactic; classify_function = (fun o -> Dispose)} +let warn_deprecated_implicit_tactic = + CWarnings.create ~name:"deprecated-implicit-tactic" ~category:"deprecated" + (fun () -> strbrk "Implicit tactics are deprecated") + let declare_implicit_tactic tac = + let () = warn_deprecated_implicit_tactic () in Lib.add_anonymous_leaf (inImplicitTactic (Some (Tacintern.glob_tactic tac))) let clear_implicit_tactic () = + let () = warn_deprecated_implicit_tactic () in Lib.add_anonymous_leaf (inImplicitTactic None) VERNAC COMMAND EXTEND ImplicitTactic CLASSIFIED AS SIDEFF -- cgit v1.2.3