[doc] Address feedback on doc writer guide

Co-Authored-By: @Zimmi48

1 files changed, 16 insertions, 8 deletions

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``::