[doc] Address feedback on doc writer guide

Co-Authored-By: @Zimmi48

7 files changed, 70 insertions, 281 deletions

diff --git a/doc/sphinx/MIGRATING b/doc/sphinx/MIGRATING
deleted file mode 100644
index fa6fe1537..000000000
--- a/doc/sphinx/MIGRATING
+++ /dev/null
@@ -1,238 +0,0 @@
-How to migrate the Coq Reference Manual to Sphinx
-=================================================
-
-# Install Python3 packages (requires Python 3, python3-pip, python3-setuptools)
-
-  * pip3 install bs4 sphinx sphinx_rtd_theme pexpect antlr4-python3-runtime sphinxcontrib-bibtex
-
-# You may want to do this under a virtualenv, particularly if you end up with issues finding sphinxcontrib.bibtex. http://docs.python-guide.org/en/latest/dev/virtualenvs/
-
-  * pip3 install virtualenv
-  * virtualenv coqsphinxing # you may want to use -p to specify the python version
-  * source coqsphinxing/bin/activate # activate the virtual environment
-
-# After activating the virtual environment you can run the above pip3 command to install sphinx. You will have to activate the virtual environment before building the docs in your session.
-
-# Add this Elisp code to .emacs, if you're using emacs (recommended):
-
- (defun sphinx/quote-coq-refman-region (left right &optional beg end count)
-   (unless beg
-     (if (region-active-p)
-         (setq beg (region-beginning) end (region-end))
-       (setq beg (point) end nil)))
-   (unless count
-     (setq count 1))
-   (save-excursion
-     (goto-char (or end beg))
-     (dotimes (_ count) (insert right)))
-   (save-excursion
-     (goto-char beg)
-     (dotimes (_ count) (insert left)))
-   (if (and end (characterp left)) ;; Second test handles the ::`` case
-       (goto-char (+ (* 2 count) end))
-     (goto-char (+ count beg))))
-
- (defun sphinx/coqtop (beg end)
-   (interactive (list (region-beginning) (region-end)))
-   (replace-regexp "^Coq < " "      " nil beg end)
-   (indent-rigidly beg end -3)
-   (goto-char beg)
-   (insert ".. coqtop:: all\n\n"))
-
- (defun sphinx/rst-coq-action ()
-   (interactive)
-   (pcase (read-char "Command?")
-     (?g (sphinx/quote-coq-refman-region ":g:`" "`"))
-     (?n (sphinx/quote-coq-refman-region ":n:`" "`"))
-     (?t (sphinx/quote-coq-refman-region ":token:`" "`"))
-     (?m (sphinx/quote-coq-refman-region ":math:`" "`"))
-     (?: (sphinx/quote-coq-refman-region "::`" "`"))
-     (?` (sphinx/quote-coq-refman-region "``" "``"))
-     (?c (sphinx/coqtop (region-beginning) (region-end)))))
-
- (global-set-key (kbd "<f12>") #'sphinx/rst-coq-action)
-
- With this code installed, you can hit "F12" followed by an appropriate key to do quick markup of text
- (this will make more sense once you've started editing the text).
-
-# Fork the Coq repo, if needed:
-
- https://github.com/coq/coq
-
-# Clone the repo to your work machine
-
-# Add Maxime Dénès's repo as a remote:
-
- git remote add sphinx https://github.com/maximedenes/coq.git
-
-  (or choose a name other than "sphinx")
-
- Verify with:
-
- git remote -v
-
-# Fetch from the remote
-
- git fetch sphinx
-
-# Checkout the sphinx-doc branch
-
-   git checkout sphinx-doc
-
-  You should pull from the repo from time to time to keep your local copy up-to-date:
-
-   git pull sphinx sphinx-doc
-
-  You may want to create a new branch to do your work in.
-
-# Choose a Reference Manual chapter to work on at
-
-    https://docs.google.com/document/d/1Yo7dV4OI0AY9Di-lsEQ3UTmn5ygGLlhxjym7cTCMCWU
-
-# For each chapter, raw ReStructuredText (the Sphinx format), created by the "html2rest" utility,
-   is available in the directory porting/raw-rst/
-
-  Elsewhere, depending on the chapter, there should be an almost-empty template file already created,
-   which is in the location where the final version should go
-
-# Manually edit the .rst file, place it in the correct location
-
-  There are small examples in sphinx/porting/, a larger example in language/gallina-extensions.rst
-
-  (N.B.: the migration is a work-in-progress, your suggestions are welcome)
-
-  Find the chapter you're working on from the online manual at https://coq.inria.fr/distrib/current/refman/.
-  At the top of the file, after the chapter heading, add:
-
-    :Source: https://coq.inria.fr/distrib/current/refman/the-chapter-file.html
-    :Converted by: Your Name
-
-  N.B.: These source and converted-by annotations should help for the migration phase. Later on,
-  those annotations will be removed, and contributors will be mentioned in the Coq credits.
-
-  Remove chapter numbers
-
-  Replace section, subsection numbers with reference labels:
-
-    .. _some-reference-label:
-
-  Place the label before the section or subsection, followed by a blank line.
-
-  Note the leading underscore. Use :ref:`some_reference-label` to refer to such a label; note the leading underscore is omitted.
-  Many cross-references may be to other chapters. If the required label exists, use it. Otherwise, use a dummy reference of the form
-  `TODO-n.n.n-mnemonic` we can fixup later. Example:
-
-    :ref:`TODO-1.3.2-definitions`
-
-  We can grep for those TODOs, and the existing subsection number makes it easy to find in the exisyting manual.
-
-  For the particular case of references to chapters, we can use a
-convention for the cross-reference name, so no TODO is needed.
-
-    :ref:`thegallinaspecificationlanguage`
-
-That is, the chapter label is the chapter title, all in lower-case,
-with no spaces or punctuation. For chapters with subtitles marked with
-a ":", like those for Omega and Nsatz, use just the chapter part
-preceding the ":". These labels should already be in the
-placeholder .rst files for each chapter.
-
-
-  You can also label other items, like grammars, with the same syntax. To refer to such labels, not involving a
-  section or subsection, use the syntax
-
-    :ref:`Some link text <label-name>`
-
-  Yes, the angle-brackets are needed here!
-
-  For bibliographic references (those in biblio.bib), use :cite:`thecitation`.
-
-  Grammars will get mangled by the translation. Look for "productionlist" in the examples, also see
-  http://www.sphinx-doc.org/en/stable/markup/para.html.
-
-  For Coq examples that appear, look at the "coqtop" syntax in porting/tricky-bits.rst. The Sphinx
-  script will run coqtop on those examples, and can show the output (or not).
-
-  The file replaces.rst contains replacement definitions for some items that are clumsy to write out otherwise.
-  Use
-
-    .. include:: replaces.rst
-
-  to gain access to those definitions in your file (you might need a path prefix). Some especially-important
-  replacements are |Cic|, |Coq|, |CoqIDE|, and |Gallina|, which display those names in small-caps. Please use them,
-  so that they're rendered consistently.
-
-  Similarly, there are some LaTeX macros in preamble.rst that can be useful.
-
-  Conventions:
-
-    - Keywords and other literal text is double-backquoted (e.g. ``Module``, ``Section``, ``(``, ``,``).
-
-    - Metavariables are single-backquotes (e.g. `term`, `ident`)
-
-    - Use the cmd directive for Vernacular commands, like:
-
-      .. cmd:: Set Printing All.
-
-      Within this directive, prefix metavariables (ident, term) with @:
-
-      .. cmd:: Add Printing Let @ident.
-
-      There's also the "cmdv" directive for variants of a command.
-
-    - Use the "exn" and "warn" directives for errors and warnings:
-
-      .. exn:: Something's not right.
-      .. warn:: You shouldn't do that.
-
-    - Use the "example" directive for examples
-
-    - Use the "g" role for inline Gallina, like :g:`fun x => x`
-
-    - Use code blocks for blocks of Gallina. You can use a double-colon at the end of a line::
-
-        your code here
-
-      which prints a single colon, or put the double-colon on a newline.
-
-::
-
-        your other code here
-
-# Making changes to the text
-
-  The goal of the migration is simply to change the storage format from LaTeX to ReStructuredText. The goal is not
-  to make any organizational or other substantive changes to the text. If you do notice nits (misspellings, wrong
-  verb tense, and so on), please do change them. For example, the programming language that Coq is written in is these days
-  called "OCaml", and there are mentions of the older name "Objective Caml" in the reference manual that should be changed.
-
-# Build, view the manual
-
-  In the root directory of your local repo, run "make sphinx". You can view the result in a browser by loading the HTML file
-  associated with your chapter, which will be contained in the directory doc/sphinx/_build/html/ beneath the repo root directory.
-  Make any changes you need until there are no build warnings and the output is perfect. :-)
-
-# Creating pull requests
-
-  When your changes are done, commit them, push to your fork:
-
-   git commit -m "useful commit message" file
-   git push origin sphinx-doc
-
-  (or push to another branch, if you've created one). Then go to your GitHub
-  fork and create a pull request against Maxime's sphinx-doc
-  branch. If your commit is recent, you should see a link on your
-  fork's code page to do that. Otherwise, you may need to go to your
-  branch on GitHub to do that.
-
-# Issues/Questions/Suggestions
-
-  As the migration proceeds, if you have technical issues, have a more general question, or want to suggest something, please contact:
-
-    Paul Steckler <steck@stecksoft.com>
-    Maxime Dénès <maxime.denes@inria.fr>
-
-# Issues
-
-  Should the stuff in replaces.rst go in preamble.rst?
-  In LaTeX, some of the grammars add productions to existing nonterminals, like term ++= ... . How to indicate that?
diff --git a/doc/sphinx/README.rst b/doc/sphinx/README.rst
index b22c5086c..4dba01216 100644
--- a/doc/sphinx/README.rst
+++ b/doc/sphinx/README.rst
@@ -3,16 +3,17 @@
 =============================
 
 ..
-   This README is auto-generated from the coqrst docs; use ``./regen_readme.py`` to rebuild the it.
+   README.rst is auto-generated from README.template.rst and the coqrst docs;
+   use ``doc/tools/coqrst/regen_readme.py`` to rebuild it.
 
-Coq's documentation is written in `reStructuredText <http://www.sphinx-doc.org/en/master/usage/restructuredtext/basics.html>`_ (“reST”), and compiled with `Sphinx <http://www.sphinx-doc.org/en/master/>`_.
+Coq's reference manual is written in `reStructuredText <http://www.sphinx-doc.org/en/master/usage/restructuredtext/basics.html>`_ (“reST”), and compiled with `Sphinx <http://www.sphinx-doc.org/en/master/>`_.
 
-In addition to standard reST directives (a directive is similar to a LaTeX environment) and roles (a role is similar to a LaTeX command), the ``coqrst`` plugin loaded by the documentation uses a custom *Coq domain* —a set of Coq-specific directives that define *objects* like tactics, commands (vernacs), warnings, etc.—, some custom *directives*, and a few custom *roles*.  Finally, this manual uses a small DSL to describe tactic invocations and commands.
+In addition to standard reST directives (a directive is similar to a LaTeX environment) and roles (a role is similar to a LaTeX command), the ``coqrst`` plugin loaded by the documentation uses a custom *Coq domain* — a set of Coq-specific directives that define *objects* like tactics, commands (vernacs), warnings, etc. —, some custom *directives*, and a few custom *roles*.  Finally, this manual uses a small DSL to describe tactic invocations and commands.
 
 Coq objects
 ===========
 
-Our Coq domain define the following 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 <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
@@ -24,7 +25,7 @@ Our Coq domain define the following objects.  Each object has a “signature”
 
 Objects are automatically collected into indices, and can be linked to using the role version of the object's directive. For example, you could link to the tactic variant above using ``:tacv:`simpl_at```, and to its exception using ``:exn:`Too few occurrences```.
 
-Names (link targets) are auto-generated for most simple objects, though they can always be overwritten using a `:name:` option, as shown above.
+Names (link targets) are auto-generated for most simple objects, though they can always be overwritten using a ``:name:`` option, as shown above.
 
 - Options, errors, warnings have their name set to their signature, with ``...`` replacing all notation bits.  For example, the auto-generated name of ``.. exn:: @qualid is not a module`` is ``... is not a module``, and a link to it would take the form ``:exn:`... is not a module```.
 - Vernacs (commands) have their name set to the first word of their signature.  For example, the auto-generated name of ``Axiom @ident : @term`` is ``Axiom``, and a link to it would take the form ``:cmd:`Axiom```.
@@ -33,10 +34,10 @@ 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 <https://github.com/coq/coq/blob/master/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 (``@id``, ``@num``, ``@tactic``)
+  A placeholder (``@ident``, ``@num``, ``@tactic``\ …)
 
 ``{? …}``
   an optional block
@@ -45,7 +46,7 @@ The signatures of most objects can be written using a succinct DSL for Coq notat
   an optional (``*``) or mandatory (``+``) block that can be repeated, with repetitions separated by spaces
 
 ``{*, …}``, ``{+, …}``
-  an optional or mandatory repeatable block, with repetitions separated by spaces
+  an optional or mandatory repeatable block, with repetitions separated by commas
 
 ``%|``, ``%{``, …
   an escaped character (rendered without the leading ``%``)
@@ -78,8 +79,8 @@ Here is the list of all objects of the Coq domain (The symbol :black_nib: indica
 
        .. cmd:: Axiom @ident : @term.
 
-          This command links *term* to the name *ident* as its specification in
-          the global context. The fact asserted by *term* is thus assumed as a
+          This command links :token:`term` to the name :token:`term` as its specification in
+          the global context. The fact asserted by :token:`term` is thus assumed as a
           postulate.
 
           .. cmdv:: Parameter @ident : @term.
@@ -99,7 +100,7 @@ Here is the list of all objects of the Coq domain (The symbol :black_nib: indica
 
           .. exn:: Proof is not complete
 
-             Raised is :n:`@tactic` does not fully solve the goal.
+             Raised if :n:`@tactic` does not fully solve the goal.
 
 ``.. opt::`` :black_nib: A Coq option.
     Example::
@@ -154,8 +155,8 @@ Here is the list of all objects of the Coq domain (The symbol :black_nib: indica
 
        .. warn:: Ambiguous path
 
-         When the coercion `qualid` is added to the inheritance graph, non
-         valid coercion paths are ignored.
+          When the coercion :token:`qualid` is added to the inheritance graph, non
+          valid coercion paths are ignored.
 
 Coq directives
 ==============
@@ -191,6 +192,10 @@ In addition to the objects above, the ``coqrst`` Sphinx plugin defines the follo
       - ``undo``: Send an ``Undo n`` (``n`` = number of sentences) command after
         running all the commands in this block
 
+    ``coqtop``\ 's state is preserved across consecutive ``.. coqtop::`` blocks
+    of the same document (``coqrst`` creates a single ``coqtop`` process per
+    reST source file).  Use the ``reset`` option to reset Coq's state.
+
 ``.. coqdoc::`` A reST directive to display Coqtop-formatted source code.
     Usage::
 
@@ -263,7 +268,8 @@ In addition to the objects and directives above, the ``coqrst`` Sphinx plugin de
        :g:`forall (x: t), P(x)`
 
 ``:n:`` Any text using the notation syntax (``@id``, ``{+, …}``, etc.).
-    Use this to explain tactic equivalences (for example, you might write this::
+    Use this to explain tactic equivalences.  For example, you might write
+    this::
 
        :n:`generalize @term as @ident` is just like :n:`generalize @term`, but
        it names the introduced hypothesis :token:`ident`.
@@ -290,7 +296,15 @@ In addition to the objects and directives above, the ``coqrst`` Sphinx plugin de
 Tips and tricks
 ===============
 
-The ``dev/tools/coqdev.el`` folder contains a convenient Emacs function to quickly insert Sphinx roles and quotes.  It takes a single character (one of ``gntm:```), and inserts one of `:g:`, `:n:`, `:t:`, or an arbitrary role, or double quotes.  You can also select a region of text, and wrap it in single or double backticks using that function.
+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>`_.
+
+Emacs
+-----
+
+The ``dev/tools/coqdev.el`` folder contains a convenient Emacs function to quickly insert Sphinx roles and quotes.  It takes a single character (one of ``gntm:```), and inserts one of ``:g:``, ``:n:``, ``:t:``, or an arbitrary role, or double quotes.  You can also select a region of text, and wrap it in single or double backticks using that function.
 
 Use the following snippet to bind it to :kbd:`F12` in ``rst-mode``::
 
diff --git a/doc/sphinx/README.template.rst b/doc/sphinx/README.template.rst
index 10a4fcadf..11bcbb083 100644
--- a/doc/sphinx/README.template.rst
+++ b/doc/sphinx/README.template.rst
@@ -6,14 +6,14 @@
    README.rst is auto-generated from README.template.rst and the coqrst docs;
    use ``doc/tools/coqrst/regen_readme.py`` to rebuild it.
 
-Coq's documentation is written in `reStructuredText <http://www.sphinx-doc.org/en/master/usage/restructuredtext/basics.html>`_ (“reST”), and compiled with `Sphinx <http://www.sphinx-doc.org/en/master/>`_.
+Coq's reference manual is written in `reStructuredText <http://www.sphinx-doc.org/en/master/usage/restructuredtext/basics.html>`_ (“reST”), and compiled with `Sphinx <http://www.sphinx-doc.org/en/master/>`_.
 
-In addition to standard reST directives (a directive is similar to a LaTeX environment) and roles (a role is similar to a LaTeX command), the ``coqrst`` plugin loaded by the documentation uses a custom *Coq domain* —a set of Coq-specific directives that define *objects* like tactics, commands (vernacs), warnings, etc.—, some custom *directives*, and a few custom *roles*.  Finally, this manual uses a small DSL to describe tactic invocations and commands.
+In addition to standard reST directives (a directive is similar to a LaTeX environment) and roles (a role is similar to a LaTeX command), the ``coqrst`` plugin loaded by the documentation uses a custom *Coq domain* — a set of Coq-specific directives that define *objects* like tactics, commands (vernacs), warnings, etc. —, some custom *directives*, and a few custom *roles*.  Finally, this manual uses a small DSL to describe tactic invocations and commands.
 
 Coq objects
 ===========
 
-Our Coq domain define the following 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 <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
@@ -25,7 +25,7 @@ Our Coq domain define the following objects.  Each object has a “signature”
 
 Objects are automatically collected into indices, and can be linked to using the role version of the object's directive. For example, you could link to the tactic variant above using ``:tacv:`simpl_at```, and to its exception using ``:exn:`Too few occurrences```.
 
-Names (link targets) are auto-generated for most simple objects, though they can always be overwritten using a `:name:` option, as shown above.
+Names (link targets) are auto-generated for most simple objects, though they can always be overwritten using a ``:name:`` option, as shown above.
 
 - Options, errors, warnings have their name set to their signature, with ``...`` replacing all notation bits.  For example, the auto-generated name of ``.. exn:: @qualid is not a module`` is ``... is not a module``, and a link to it would take the form ``:exn:`... is not a module```.
 - Vernacs (commands) have their name set to the first word of their signature.  For example, the auto-generated name of ``Axiom @ident : @term`` is ``Axiom``, and a link to it would take the form ``:cmd:`Axiom```.
@@ -34,10 +34,10 @@ 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 <https://github.com/coq/coq/blob/master/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 (``@id``, ``@num``, ``@tactic``)
+  A placeholder (``@ident``, ``@num``, ``@tactic``\ …)
 
 ``{? …}``
   an optional block
@@ -46,7 +46,7 @@ The signatures of most objects can be written using a succinct DSL for Coq notat
   an optional (``*``) or mandatory (``+``) block that can be repeated, with repetitions separated by spaces
 
 ``{*, …}``, ``{+, …}``
-  an optional or mandatory repeatable block, with repetitions separated by spaces
+  an optional or mandatory repeatable block, with repetitions separated by commas
 
 ``%|``, ``%{``, …
   an escaped character (rendered without the leading ``%``)
@@ -86,7 +86,15 @@ In addition to the objects and directives above, the ``coqrst`` Sphinx plugin de
 Tips and tricks
 ===============
 
-The ``dev/tools/coqdev.el`` folder contains a convenient Emacs function to quickly insert Sphinx roles and quotes.  It takes a single character (one of ``gntm:```), and inserts one of `:g:`, `:n:`, `:t:`, or an arbitrary role, or double quotes.  You can also select a region of text, and wrap it in single or double backticks using that function.
+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>`_.
+
+Emacs
+-----
+
+The ``dev/tools/coqdev.el`` folder contains a convenient Emacs function to quickly insert Sphinx roles and quotes.  It takes a single character (one of ``gntm:```), and inserts one of ``:g:``, ``:n:``, ``:t:``, or an arbitrary role, or double quotes.  You can also select a region of text, and wrap it in single or double backticks using that function.
 
 Use the following snippet to bind it to :kbd:`F12` in ``rst-mode``::
 
diff --git a/doc/sphinx/addendum/implicit-coercions.rst b/doc/sphinx/addendum/implicit-coercions.rst
index 152f4f655..09faa0676 100644
--- a/doc/sphinx/addendum/implicit-coercions.rst
+++ b/doc/sphinx/addendum/implicit-coercions.rst
@@ -140,29 +140,29 @@ Declaration of Coercions
 
   .. warn:: Ambiguous path.
 
-    When the coercion `qualid` is added to the inheritance graph, non
-    valid coercion paths are ignored; they are signaled by a warning
-    displaying these paths of the form :g:`[f₁;..;fₙ] : C >-> D`.
+     When the coercion :token:`qualid` is added to the inheritance graph, non
+     valid coercion paths are ignored; they are signaled by a warning
+     displaying these paths of the form :g:`[f₁;..;fₙ] : C >-> D`.
 
   .. cmdv:: Local Coercion @qualid : @class >-> @class
 
-    Declares the construction denoted by `qualid` as a coercion local to
-    the current section.
+     Declares the construction denoted by `qualid` as a coercion local to
+     the current section.
 
   .. cmdv:: Coercion @ident := @term
 
-    This defines `ident` just like ``Definition`` `ident` ``:=`` `term`,
-    and then declares `ident` as a coercion between it source and its target.
+     This defines `ident` just like ``Definition`` `ident` ``:=`` `term`,
+     and then declares `ident` as a coercion between it source and its target.
 
   .. cmdv:: Coercion @ident := @term : @type
 
-    This defines `ident` just like ``Definition`` `ident` : `type` ``:=`` `term`,
-    and then declares `ident` as a coercion between it source and its target.
+     This defines `ident` just like ``Definition`` `ident` : `type` ``:=`` `term`,
+     and then declares `ident` as a coercion between it source and its target.
 
   .. cmdv:: Local Coercion @ident := @term
 
-    This defines `ident` just like ``Let`` `ident` ``:=`` `term`,
-    and then declares `ident` as a coercion between it source and its target.
+     This defines `ident` just like ``Let`` `ident` ``:=`` `term`,
+     and then declares `ident` as a coercion between it source and its target.
 
 Assumptions can be declared as coercions at declaration time.
 This extends the grammar of assumptions from
diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst
index aa41f8058..4dcd7deb1 100644
--- a/doc/sphinx/language/gallina-specification-language.rst
+++ b/doc/sphinx/language/gallina-specification-language.rst
@@ -553,8 +553,8 @@ has type :token:`type`.
 
 .. cmd:: Axiom @ident : @term
 
-   This command links *term* to the name *ident* as its specification in
-   the global context. The fact asserted by *term* is thus assumed as a
+   This command links :token:`term` to the name :token:`ident` as its specification in
+   the global context. The fact asserted by :token:`term` is thus assumed as a
    postulate.
 
 .. exn:: @ident already exists.
diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py
index 3cad394e6..f8bb113a7 100644
--- a/doc/tools/coqrst/coqdomain.py
+++ b/doc/tools/coqrst/coqdomain.py
@@ -215,8 +215,8 @@ class VernacVariantObject(VernacObject):
 
        .. cmd:: Axiom @ident : @term.
 
-          This command links *term* to the name *ident* as its specification in
-          the global context. The fact asserted by *term* is thus assumed as a
+          This command links :token:`term` to the name :token:`term` as its specification in
+          the global context. The fact asserted by :token:`term` is thus assumed as a
           postulate.
 
           .. cmdv:: Parameter @ident : @term.
@@ -340,7 +340,7 @@ class ExceptionObject(NotationObject):
 
           .. exn:: Proof is not complete
 
-             Raised is :n:`@tactic` does not fully solve the goal.
+             Raised if :n:`@tactic` does not fully solve the goal.
     """
     subdomain = "exn"
     index_suffix = "(err)"
@@ -362,8 +362,8 @@ class WarningObject(NotationObject):
 
        .. warn:: Ambiguous path
 
-         When the coercion `qualid` is added to the inheritance graph, non
-         valid coercion paths are ignored.
+          When the coercion :token:`qualid` is added to the inheritance graph, non
+          valid coercion paths are ignored.
     """
     subdomain = "warn"
     index_suffix = "(warn)"
@@ -377,7 +377,8 @@ def NotationRole(role, rawtext, text, lineno, inliner, options={}, content=[]):
     #pylint: disable=unused-argument, dangerous-default-value
     """Any text using the notation syntax (``@id``, ``{+, …}``, etc.).
 
-    Use this to explain tactic equivalences (for example, you might write this::
+    Use this to explain tactic equivalences.  For example, you might write
+    this::
 
        :n:`generalize @term as @ident` is just like :n:`generalize @term`, but
        it names the introduced hypothesis :token:`ident`.
@@ -445,6 +446,10 @@ class CoqtopDirective(Directive):
       - ``reset``: Send a ``Reset Initial`` command before running this block
       - ``undo``: Send an ``Undo n`` (``n`` = number of sentences) command after
         running all the commands in this block
+
+    ``coqtop``\ 's state is preserved across consecutive ``.. coqtop::`` blocks
+    of the same document (``coqrst`` creates a single ``coqtop`` process per
+    reST source file).  Use the ``reset`` option to reset Coq's state.
     """
     has_content = True
     required_arguments = 0
diff --git a/doc/tools/coqrst/regen_readme.py b/doc/tools/coqrst/regen_readme.py
index 050ca4956..e56882a52 100755
--- a/doc/tools/coqrst/regen_readme.py
+++ b/doc/tools/coqrst/regen_readme.py
@@ -1,7 +1,7 @@
 #!/usr/bin/env python3
 # -*- coding: utf-8 -*-
 
-"""Rebuild README.rst from README.template.rst."""
+"""Rebuild sphinx/README.rst from sphinx/README.template.rst."""
 
 import re
 from os import sys, path