diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/sphinx/proof-engine/proof-handling.rst | 12 | ||||
| -rw-r--r-- | doc/sphinx/user-extensions/proof-schemes.rst | 2 |
2 files changed, 1 insertions, 13 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/user-extensions/proof-schemes.rst b/doc/sphinx/user-extensions/proof-schemes.rst index eacd7b4676..8f76085d88 100644 --- a/doc/sphinx/user-extensions/proof-schemes.rst +++ b/doc/sphinx/user-extensions/proof-schemes.rst @@ -167,7 +167,7 @@ Combined Scheme Combined Scheme tree_forest_mutind from tree_forest_ind,forest_tree_ind. - The type of tree_forest_mutrec will be: + The type of tree_forest_mutind will be: .. coqtop:: all |