4 files changed, 50 insertions, 25 deletions
diff --git a/doc/sphinx/addendum/miscellaneous-extensions.rst b/doc/sphinx/addendum/miscellaneous-extensions.rst
index 80ea8a1166..b6c35d8fa7 100644
--- a/doc/sphinx/addendum/miscellaneous-extensions.rst
+++ b/doc/sphinx/addendum/miscellaneous-extensions.rst
@@ -11,7 +11,7 @@ Program derivation
 |Coq| comes with an extension called ``Derive``, which supports program
 derivation. Typically in the style of Bird and Meertens or derivations
 of program refinements. To use the Derive extension it must first be
-required with ``Require Coq.Derive.Derive``. When the extension is loaded,
+required with ``Require Coq.derive.Derive``. When the extension is loaded,
 it provides the following command:
 
 .. cmd:: Derive @ident SuchThat @term As @ident
diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst
index 4dcd7deb13..76a016ff64 100644
--- a/doc/sphinx/language/gallina-specification-language.rst
+++ b/doc/sphinx/language/gallina-specification-language.rst
@@ -1260,6 +1260,12 @@ Chapter :ref:`Tactics`. The basic assertion command is:
       The name you provided is already defined. You have then to choose
       another name.
 
+   .. exn:: Nested proofs are not allowed unless you turn option Nested Proofs Allowed on.
+
+      You are asserting a new statement while already being in proof editing mode.
+      This feature, called nested proofs, is disabled by default.
+      To activate it, turn option :opt:`Nested Proofs Allowed` on.
+
    The following commands are synonyms of :n:`Theorem @ident {? @binders } : type`:
 
    .. cmdv:: Lemma @ident {? @binders } : @type
@@ -1339,7 +1345,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/practical-tools/coq-commands.rst b/doc/sphinx/practical-tools/coq-commands.rst
index 83dddab4f5..ad1f0caa60 100644
--- a/doc/sphinx/practical-tools/coq-commands.rst
+++ b/doc/sphinx/practical-tools/coq-commands.rst
@@ -55,15 +55,20 @@ Customization at launch time
 By resource file
 ~~~~~~~~~~~~~~~~~~~~~~~
 
-When |Coq| is launched, with either ``coqtop`` or ``coqc``, the resource file
-``$XDG_CONFIG_HOME/coq/coqrc.xxx`` is loaded, where ``$XDG_CONFIG_HOME``
+When |Coq| is launched, with either ``coqtop`` or ``coqc``, the
+resource file ``$XDG_CONFIG_HOME/coq/coqrc.xxx``, if it exists, will
+be implicitly prepended to any document read by Coq, whether it is an
+interactive session or a file to compile. Here, ``$XDG_CONFIG_HOME``
 is the configuration directory of the user (by default its home
-directory ``/.config`` and ``xxx`` is the version number (e.g. 8.8). If
+directory ``~/.config``) and ``xxx`` is the version number (e.g. 8.8). If
 this file is not found, then the file ``$XDG_CONFIG_HOME/coqrc`` is
-searched. You can also specify an arbitrary name for the resource file
+searched. If not found, it is the file ``~/.coqrc.xxx`` which is searched,
+and, if still not found, the file ``~/.coqrc``. If the latter is also
+absent, no resource file is loaded.
+You can also specify an arbitrary name for the resource file
 (see option ``-init-file`` below).
 
-This file may contain, for instance, ``Add LoadPath`` commands to add
+The resource file may contain, for instance, ``Add LoadPath`` commands to add
 directories to the load path of |Coq|. It is possible to skip the
 loading of the resource file with the option ``-q``.
 
diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst
index 892ddbc165..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.
@@ -542,23 +544,34 @@ Controlling the effect of proof editing commands
 
 .. opt:: Hyps Limit @num
 
-This option controls the maximum number of hypotheses displayed in goals
-after the application of a tactic. All the hypotheses remain usable
-in the proof development.
-When unset, it goes back to the default mode which is to print all
-available hypotheses.
+   This option controls the maximum number of hypotheses displayed in goals
+   after the application of a tactic. All the hypotheses remain usable
+   in the proof development.
+   When unset, it goes back to the default mode which is to print all
+   available hypotheses.
 
 
 .. opt:: Automatic Introduction
 
-This option controls the way binders are handled
-in assertion commands such as ``Theorem ident [binders] : form``. When the
-option is on, which is the default, binders are automatically put in
-the local context of the goal to prove.
+   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.
+
+
+.. opt:: Nested Proofs Allowed
 
-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.
+   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
@@ -570,13 +583,13 @@ to force |Coq| to optimize some of its internal data structures.
 
 .. cmd:: Optimize Proof
 
-This command forces |Coq| to shrink the data structure used to represent
-the ongoing proof.
+   This command forces |Coq| to shrink the data structure used to represent
+   the ongoing proof.
 
 
 .. cmd:: Optimize Heap
 
-This command forces the |OCaml| runtime to perform a heap compaction.
-This is in general an expensive operation.
-See: `OCaml Gc <http://caml.inria.fr/pub/docs/manual-ocaml/libref/Gc.html#VALcompact>`_
-There is also an analogous tactic :tacn:`optimize_heap`.
+   This command forces the |OCaml| runtime to perform a heap compaction.
+   This is in general an expensive operation.
+   See: `OCaml Gc <http://caml.inria.fr/pub/docs/manual-ocaml/libref/Gc.html#VALcompact>`_
+   There is also an analogous tactic :tacn:`optimize_heap`.