Document nested proofs and associated option.

CHANGES

@@ -18,6 +18,9 @@ Vernacular Commands
 
 - Removed deprecated commands Arguments Scope and Implicit Arguments
   (not the option). Use the Arguments command instead.
+- Nested proofs may be enabled through the option `Nested Proofs Allowed`.
+  By default, they are disabled and produce an error. The deprecation
+  warning which used to occur when using nested proofs has been removed.
 
 Tactics
 

doc/sphinx/language/gallina-specification-language.rst

@@ -1339,7 +1339,8 @@ using the keyword :cmd:`Qed`.
 
 .. note::
 
-   #. Several statements can be simultaneously asserted.
+   #. Several statements can be simultaneously asserted provided option
+      :opt:`Nested Proofs Allowed` was turned on.
 
    #. Not only other assertions but any vernacular command can be given
       while in the process of proving a given assertion. In this case, the

doc/sphinx/proof-engine/proof-handling.rst

@@ -113,6 +113,8 @@ list of assertion commands is given in :ref:`Assertions`. The command
       Aborts the editing of the proof named :token:`ident` (in case you have
       nested proofs).
 
+      .. seealso:: :opt:`Nested Proofs Allowed`
+
    .. cmdv:: Abort All
 
       Aborts all current goals.
@@ -561,6 +563,17 @@ Controlling the effect of proof editing commands
    has to be used to move the assumptions to the local context.
 
 
+.. opt:: Nested Proofs Allowed
+
+   When turned on (it is off by default), this option enables support for nested
+   proofs: a new assertion command can be inserted before the current proof is
+   finished, in which case Coq will temporarily switch to the proof of this
+   *nested lemma*. When the proof of the nested lemma is finished (with :cmd:`Qed`
+   or :cmd:`Defined`), its statement will be made available (as if it had been
+   proved before starting the previous proof) and Coq will switch back to the
+   proof of the previous assertion.
+
+
 Controlling memory usage
 ------------------------