[doc] More feedback on doc writer guide

Co-Authored-By: @Zimmi48

3 files changed, 38 insertions, 11 deletions

diff --git a/doc/sphinx/README.rst b/doc/sphinx/README.rst
index 4dba01216..5f2f21f2b 100644
--- a/doc/sphinx/README.rst
+++ b/doc/sphinx/README.rst
@@ -13,7 +13,7 @@ In addition to standard reST directives (a directive is similar to a LaTeX envir
 Coq objects
 ===========
 
-Our Coq domain define multiple `objects <Objects>`_.  Each object has a *signature* (think *type signature*), followed by an optional body (a description of that object).  The following example defines two objects: a variant of the ``simpl`` tactic, and an error that it may raise::
+Our Coq domain define multiple `objects`_.  Each object has a *signature* (think *type signature*), followed by an optional body (a description of that object).  The following example defines two objects: a variant of the ``simpl`` tactic, and an error that it may raise::
 
    .. tacv:: simpl @pattern at {+ @num}
       :name: simpl_at
@@ -34,7 +34,7 @@ Names (link targets) are auto-generated for most simple objects, though they can
 Notations
 ---------
 
-The signatures of most objects can be written using a succinct DSL for Coq notations (think regular expressions written with a Lispy syntax).  A typical signature might look like ``Hint Extern @num {? @pattern} => @tactic``, which means that the ``Hint Extern`` command takes a number (``num``), followed by an optional pattern, and a mandatory tactic.  The language has the following constructs (the full grammar is in `TacticNotations.g <doc/tools/coqrst/notations/TacticNotations.g>`_):
+The signatures of most objects can be written using a succinct DSL for Coq notations (think regular expressions written with a Lispy syntax).  A typical signature might look like ``Hint Extern @num {? @pattern} => @tactic``, which means that the ``Hint Extern`` command takes a number (``num``), followed by an optional pattern, and a mandatory tactic.  The language has the following constructs (the full grammar is in `TacticNotations.g </doc/tools/coqrst/notations/TacticNotations.g>`_):
 
 ``@…``
   A placeholder (``@ident``, ``@num``, ``@tactic``\ …)
@@ -279,9 +279,7 @@ In addition to the objects and directives above, the ``coqrst`` Sphinx plugin de
     creates a link to that.  When referring to a placeholder that happens to be
     a grammar production, ``:token:`…``` is typically preferable to ``:n:`@…```.
 
-``:production:`` A Sphinx role to format grammar productions not included in a
-    `productionlist` directive.
-
+``:production:`` A grammar production not included in a ``productionlist`` directive.
     Useful to informally introduce a production, as part of running text.
 
     Example::
@@ -296,10 +294,25 @@ In addition to the objects and directives above, the ``coqrst`` Sphinx plugin de
 Tips and tricks
 ===============
 
+Nested lemmas
+-------------
+
+The ``.. coqtop::`` directive does *not* reset Coq after running its contents.  That is, the following will create two nested lemmas::
+
+   .. coqtop:: all
+
+      Lemma l1: 1 + 1 = 2.
+
+   .. coqtop:: all
+
+      Lemma l2: 2 + 2 <> 1.
+
+Add either ``undo`` to the first block or ``reset`` to the second block to avoid nesting lemmas.
+
 Abbreviations and macros
 ------------------------
 
-Abbreviations and placeholders for specially-formatted names (like ``|Cic|``, ``|Coq|``, ``|CoqIDE|``, and ``|Gallina|``) are defined in a `separate file <doc/sphinx/replaces.rst>`_ included by most chapters of the manual.  Some useful LaTeX macros (like ``\alors``), are defined in `<doc/sphinx/replaces.rst>`_.
+Abbreviations and placeholders for specially-formatted names (like ``|Cic|``, ``|Coq|``, ``|CoqIDE|``, ``|Ltac|``, and ``|Gallina|``) are defined in a `separate file </doc/sphinx/replaces.rst>`_ included by most chapters of the manual.  Some useful LaTeX macros are defined in `</doc/sphinx/preamble.rst>`_.
 
 Emacs
 -----
diff --git a/doc/sphinx/README.template.rst b/doc/sphinx/README.template.rst
index 11bcbb083..203251abf 100644
--- a/doc/sphinx/README.template.rst
+++ b/doc/sphinx/README.template.rst
@@ -13,7 +13,7 @@ In addition to standard reST directives (a directive is similar to a LaTeX envir
 Coq objects
 ===========
 
-Our Coq domain define multiple `objects <Objects>`_.  Each object has a *signature* (think *type signature*), followed by an optional body (a description of that object).  The following example defines two objects: a variant of the ``simpl`` tactic, and an error that it may raise::
+Our Coq domain define multiple `objects`_.  Each object has a *signature* (think *type signature*), followed by an optional body (a description of that object).  The following example defines two objects: a variant of the ``simpl`` tactic, and an error that it may raise::
 
    .. tacv:: simpl @pattern at {+ @num}
       :name: simpl_at
@@ -34,7 +34,7 @@ Names (link targets) are auto-generated for most simple objects, though they can
 Notations
 ---------
 
-The signatures of most objects can be written using a succinct DSL for Coq notations (think regular expressions written with a Lispy syntax).  A typical signature might look like ``Hint Extern @num {? @pattern} => @tactic``, which means that the ``Hint Extern`` command takes a number (``num``), followed by an optional pattern, and a mandatory tactic.  The language has the following constructs (the full grammar is in `TacticNotations.g <doc/tools/coqrst/notations/TacticNotations.g>`_):
+The signatures of most objects can be written using a succinct DSL for Coq notations (think regular expressions written with a Lispy syntax).  A typical signature might look like ``Hint Extern @num {? @pattern} => @tactic``, which means that the ``Hint Extern`` command takes a number (``num``), followed by an optional pattern, and a mandatory tactic.  The language has the following constructs (the full grammar is in `TacticNotations.g </doc/tools/coqrst/notations/TacticNotations.g>`_):
 
 ``@…``
   A placeholder (``@ident``, ``@num``, ``@tactic``\ …)
@@ -86,10 +86,25 @@ In addition to the objects and directives above, the ``coqrst`` Sphinx plugin de
 Tips and tricks
 ===============
 
+Nested lemmas
+-------------
+
+The ``.. coqtop::`` directive does *not* reset Coq after running its contents.  That is, the following will create two nested lemmas::
+
+   .. coqtop:: all
+
+      Lemma l1: 1 + 1 = 2.
+
+   .. coqtop:: all
+
+      Lemma l2: 2 + 2 <> 1.
+
+Add either ``undo`` to the first block or ``reset`` to the second block to avoid nesting lemmas.
+
 Abbreviations and macros
 ------------------------
 
-Abbreviations and placeholders for specially-formatted names (like ``|Cic|``, ``|Coq|``, ``|CoqIDE|``, and ``|Gallina|``) are defined in a `separate file <doc/sphinx/replaces.rst>`_ included by most chapters of the manual.  Some useful LaTeX macros (like ``\alors``), are defined in `<doc/sphinx/replaces.rst>`_.
+Abbreviations and placeholders for specially-formatted names (like ``|Cic|``, ``|Coq|``, ``|CoqIDE|``, ``|Ltac|``, and ``|Gallina|``) are defined in a `separate file </doc/sphinx/replaces.rst>`_ included by most chapters of the manual.  Some useful LaTeX macros are defined in `</doc/sphinx/preamble.rst>`_.
 
 Emacs
 -----
diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py
index f8bb113a7..606d725bf 100644
--- a/doc/tools/coqrst/coqdomain.py
+++ b/doc/tools/coqrst/coqdomain.py
@@ -829,8 +829,7 @@ class IndexXRefRole(XRefRole):
         return title, target
 
 def GrammarProductionRole(typ, rawtext, text, lineno, inliner, options={}, content=[]):
-    """A Sphinx role to format grammar productions not included in a
-    `productionlist` directive.
+    """A grammar production not included in a ``productionlist`` directive.
 
     Useful to informally introduce a production, as part of running text.