diff options
Diffstat (limited to 'doc/sphinx/proof-engine')
| -rw-r--r-- | doc/sphinx/proof-engine/proof-handling.rst | 12 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/tactics.rst | 26 |
2 files changed, 0 insertions, 38 deletions
diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst index 741f9fe5b0..0b059f92ee 100644 --- a/doc/sphinx/proof-engine/proof-handling.rst +++ b/doc/sphinx/proof-engine/proof-handling.rst @@ -758,18 +758,6 @@ Controlling the effect of proof editing commands available hypotheses. -.. flag:: Automatic Introduction - - This option controls the way binders are handled - in assertion commands such as :n:`Theorem @ident {? @binders} : @term`. When the - option is on, which is the default, binders are automatically put in - the local context of the goal to prove. - - When the option is off, binders are discharged on the statement to be - proved and a tactic such as :tacn:`intro` (see Section :ref:`managingthelocalcontext`) - has to be used to move the assumptions to the local context. - - .. flag:: Nested Proofs Allowed When turned on (it is off by default), this option enables support for nested 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 |