Remove outdated references to productionlist.

4 files changed, 6 insertions, 12 deletions

diff --git a/.gitignore b/.gitignore
index 92e9fd2105..bdd692420f 100644
--- a/.gitignore
+++ b/.gitignore
@@ -113,7 +113,6 @@ doc/stdlib/FullLibrary.coqdoc.tex
 doc/stdlib/html/
 doc/stdlib/index-body.html
 doc/stdlib/index-list.html
-doc/tools/docgram/productionlistGrammar
 doc/tools/docgram/editedGrammar
 doc/tools/docgram/prodnGrammar
 doc/unreleased.rst
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
-    <http://www.sphinx-doc.org/en/stable/markup/para.html#directive-productionlist>`_
-    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 <term>` to display "text"
diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py
index d8caf4efe2..cffe196b77 100644
--- a/doc/tools/coqrst/coqdomain.py
+++ b/doc/tools/coqrst/coqdomain.py
@@ -1169,7 +1169,7 @@ class StdGlossaryIndex(Index):
         return content, False
 
 def GrammarProductionRole(typ, rawtext, text, lineno, inliner, options={}, content=[]):
-    """A grammar production not included in a ``productionlist`` directive.
+    """A grammar production not included in a ``prodn`` directive.
 
     Useful to informally introduce a production, as part of running text.
 
@@ -1177,10 +1177,8 @@ def GrammarProductionRole(typ, rawtext, text, lineno, inliner, options={}, conte
 
        :production:`string` indicates a quoted string.
 
-    You're not likely to use this role very commonly; instead, use a
-    `production list
-    <http://www.sphinx-doc.org/en/stable/markup/para.html#directive-productionlist>`_
-    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:`…```.
     """
     #pylint: disable=dangerous-default-value, unused-argument
     env = inliner.document.settings.env
diff --git a/doc/tools/docgram/README.md b/doc/tools/docgram/README.md
index 14f87e5885..4d38955fa8 100644
--- a/doc/tools/docgram/README.md
+++ b/doc/tools/docgram/README.md
@@ -2,7 +2,6 @@
 
 `doc_grammar` extracts Coq's grammar from `.mlg` files, edits it and inserts it
 into `.rst` files.  The tool inserts `prodn` directives for  grammar productions.
-(`productionlist` are gradually being replaced by `prodn` in the manual.)
 It also updates `tacn` and `cmd` directives when they can be unambiguously matched to
 productions of the grammar (in practice, that's probably almost always).
 `tacv` and `cmdv` directives are not updated because matching them appears to require