diff options
| author | Pierre-Marie Pédrot | 2018-11-19 13:38:48 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-11-19 13:38:48 +0100 |
| commit | 6498a76f9755a9c82a04f0c4e088bc809eedede5 (patch) | |
| tree | 2db09d01926223466adfa5864573fb27960a38ea /doc | |
| parent | d73fee2674999225ce59cc0a9f61dfafe99d7689 (diff) | |
| parent | 177f7fa97dc7a2c4459f1a1047dec801ff0c65c0 (diff) | |
Merge PR #9001: [options] Remove deprecated option automatic introduction.
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/sphinx/proof-engine/proof-handling.rst | 12 |
1 files changed, 0 insertions, 12 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 |