diff options
| author | Pierre-Marie Pédrot | 2018-10-19 15:10:29 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-11-16 11:45:55 +0100 |
| commit | ad6d5a658806d1c0cf46a39f58113bfbd2ac808d (patch) | |
| tree | f57ac270631b9cd2ac00d22651902c6b2f0905e3 /doc | |
| parent | 778213b89d893b55e572fc1813c7209d647ed6b0 (diff) | |
Remove the implicit tactic feature following #7229.
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/sphinx/language/gallina-extensions.rst | 4 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/tactics.rst | 26 |
2 files changed, 0 insertions, 30 deletions
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 <typeclasses>` or - :ref:`tactics-in-terms <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 |