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 +++++ test-suite/bugs/closed/4882.v | 50 ------------------------------------- test-suite/success/ImplicitTactic.v | 16 ------------ theories/Logic/Diaconescu.v | 2 -- 4 files changed, 6 insertions(+), 68 deletions(-) delete mode 100644 test-suite/bugs/closed/4882.v delete mode 100644 test-suite/success/ImplicitTactic.v diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4 index c5254b37c9..2a6e8c060a 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 diff --git a/test-suite/bugs/closed/4882.v b/test-suite/bugs/closed/4882.v deleted file mode 100644 index 8c26af708b..0000000000 --- a/test-suite/bugs/closed/4882.v +++ /dev/null @@ -1,50 +0,0 @@ - -Definition Foo {T}{a : T} : T := a. - -Module A. - - Declare Implicit Tactic eauto. - - Goal forall A (x : A), A. - intros. - apply Foo. (* Check defined evars are normalized *) - (* Qed. *) - Abort. - -End A. - -Module B. - - Definition Foo {T}{a : T} : T := a. - - Declare Implicit Tactic eassumption. - - Goal forall A (x : A), A. - intros. - apply Foo. - (* Qed. *) - Abort. - -End B. - -Module C. - - Declare Implicit Tactic first [exact True|assumption]. - - Goal forall (x : True), True. - intros. - apply (@Foo _ _). - Qed. - -End C. - -Module D. - - Declare Implicit Tactic assumption. - - Goal forall A (x : A), A. - intros. - exact _. - Qed. - -End D. diff --git a/test-suite/success/ImplicitTactic.v b/test-suite/success/ImplicitTactic.v deleted file mode 100644 index d8fa3043de..0000000000 --- a/test-suite/success/ImplicitTactic.v +++ /dev/null @@ -1,16 +0,0 @@ -(* A Wiedijk-Cruz-Filipe style tactic for solving implicit arguments *) - -(* Declare a term expression with a hole *) -Parameter quo : nat -> forall n:nat, n<>0 -> nat. -Notation "x / y" := (quo x y _) : nat_scope. - -(* Declare the tactic for resolving implicit arguments still - unresolved after type-checking; it must complete the subgoal to - succeed *) -Declare Implicit Tactic assumption. - -Goal forall n d, d<>0 -> { q:nat & { r:nat | d * q + r = n }}. -intros. -(* Here, assumption is used to solve the implicit argument of quo *) -exists (n / d). - diff --git a/theories/Logic/Diaconescu.v b/theories/Logic/Diaconescu.v index 3317766c96..66e82ddbf4 100644 --- a/theories/Logic/Diaconescu.v +++ b/theories/Logic/Diaconescu.v @@ -234,8 +234,6 @@ Qed. (** An alternative more concise proof can be done by directly using the guarded relational choice *) -Declare Implicit Tactic auto. - Lemma proof_irrel_rel_choice_imp_eq_dec' : a1=a2 \/ ~a1=a2. Proof. assert (decide: forall x:A, x=a1 \/ x=a2 -> -- cgit v1.2.3 From 2eecd666a45a79241f0aadb9493ae8ef9cc9795e Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 12 Apr 2018 17:11:34 +0200 Subject: Documenting the deprecation. --- CHANGES | 2 ++ doc/sphinx/language/gallina-extensions.rst | 1 + doc/sphinx/proof-engine/tactics.rst | 25 +++++++++++++++---------- 3 files changed, 18 insertions(+), 10 deletions(-) diff --git a/CHANGES b/CHANGES index a5a5afcbf4..9f53f589e4 100644 --- a/CHANGES +++ b/CHANGES @@ -23,6 +23,8 @@ Tactics - Option "Ltac Debug" now applies also to terms built using Ltac functions. +- Deprecated the Implicit Tactic family of commands. + Tools - Coq_makefile lets one override or extend the following variables from diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index 6ea1c162f9..ff5d352c99 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -2240,6 +2240,7 @@ This option (off by default) activates the full display of how the context of an existential variable is instantiated at each of the occurrences of the existential variable. +.. _tactics-in-terms: Solving existential variables using tactics ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 051c28f910..da63d2c30e 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -3703,19 +3703,24 @@ Setting implicit automation tactics time the term argument of a tactic has one of its holes not fully resolved. - .. example:: + .. deprecated:: 8.9 - .. coqtop:: all + This command is deprecated. Use :ref:`typeclasses ` or + :ref:`tactics-in-terms ` instead. - Parameter quo : nat -> forall n:nat, n<>0 -> nat. - Notation "x // y" := (quo x y _) (at level 40). - Declare Implicit Tactic assumption. - Goal forall n m, m<>0 -> { q:nat & { r | q * m + r = n } }. - intros. - exists (n // m). + .. example:: + + .. coqtop:: all + + Parameter quo : nat -> forall n:nat, n<>0 -> nat. + Notation "x // y" := (quo x y _) (at level 40). + Declare Implicit Tactic assumption. + Goal forall n m, m<>0 -> { q:nat & { r | q * m + r = n } }. + intros. + exists (n // m). - The tactic ``exists (n // m)`` did not fail. The hole was solved - by ``assumption`` so that it behaved as ``exists (quo n m H)``. + The tactic ``exists (n // m)`` did not fail. The hole was solved + by ``assumption`` so that it behaved as ``exists (quo n m H)``. .. _decisionprocedures: -- cgit v1.2.3