From 177f7fa97dc7a2c4459f1a1047dec801ff0c65c0 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 15 Nov 2018 04:18:36 +0100
Subject: [options] Remove deprecated option automatic introduction.

---
 doc/sphinx/proof-engine/proof-handling.rst | 12 ------------
 1 file changed, 12 deletions(-)

(limited to 'doc')

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
-- 
cgit v1.2.3