From ad6d5a658806d1c0cf46a39f58113bfbd2ac808d Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 19 Oct 2018 15:10:29 +0200 Subject: Remove the implicit tactic feature following #7229. --- doc/sphinx/language/gallina-extensions.rst | 4 ---- doc/sphinx/proof-engine/tactics.rst | 26 -------------------------- 2 files changed, 30 deletions(-) (limited to 'doc') diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index 9dae7fd102..3ddfc9aec1 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -2247,7 +2247,3 @@ expression as described in :ref:`ltac`. This construction is useful when one wants to define complicated terms using highly automated tactics without resorting to writing the proof-term by means of the interactive proof engine. - -This mechanism is comparable to the ``Declare Implicit Tactic`` command -defined at :ref:`tactics-implicit-automation`, except that the used -tactic is local to each hole instead of being declared globally. diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 457f9b2efa..041f1bc966 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -3745,32 +3745,6 @@ Setting implicit automation tactics Combines in a single line ``Proof with`` and ``Proof using``, see :ref:`proof-editing-mode` - .. cmd:: Declare Implicit Tactic @tactic - - This command declares a tactic to be used to solve implicit arguments - that Coq does not know how to solve by unification. It is used every - time the term argument of a tactic has one of its holes not fully - resolved. - - .. deprecated:: 8.9 - - This command is deprecated. Use :ref:`typeclasses ` or - :ref:`tactics-in-terms ` instead. - - .. 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)``. - .. _decisionprocedures: Decision procedures -- cgit v1.2.3