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 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'doc/sphinx/language')

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