From c9b4073104385f6079f260c5183bb3a6a989b7d9 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Tue, 15 May 2018 11:30:24 +0200
Subject: Document nested proofs and associated option.

---
 doc/sphinx/language/gallina-specification-language.rst |  3 ++-
 doc/sphinx/proof-engine/proof-handling.rst             | 13 +++++++++++++
 2 files changed, 15 insertions(+), 1 deletion(-)

(limited to 'doc')

diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst
index 4dcd7deb13..d170431058 100644
--- a/doc/sphinx/language/gallina-specification-language.rst
+++ b/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
diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst
index 6d0b277281..eba0db3ff5 100644
--- a/doc/sphinx/proof-engine/proof-handling.rst
+++ b/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
 ------------------------
 
-- 
cgit v1.2.3