From 795af932ef6606ba8385448244f60c728e9abdbd Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Fri, 11 Sep 2020 12:39:39 +0200 Subject: Remove outdated references to productionlist. --- doc/sphinx/README.rst | 8 +++----- 1 file changed, 3 insertions(+), 5 deletions(-) (limited to 'doc/sphinx') diff --git a/doc/sphinx/README.rst b/doc/sphinx/README.rst index f91874d74d..d799ecfe83 100644 --- a/doc/sphinx/README.rst +++ b/doc/sphinx/README.rst @@ -346,17 +346,15 @@ 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 grammar production not included in a ``productionlist`` directive. +``:production:`` A grammar production not included in a ``prodn`` directive. Useful to informally introduce a production, as part of running text. Example:: :production:`string` indicates a quoted string. - You're not likely to use this role very commonly; instead, use a - `production list - `_ - and reference its tokens using ``:token:`…```. + You're not likely to use this role very commonly; instead, use a ``prodn`` + directive and reference its tokens using ``:token:`…```. ``:gdef:`` Marks the definition of a glossary term inline in the text. Matching :term:`XXX` constructs will link to it. Use the form :gdef:`text ` to display "text" -- cgit v1.2.3