Merge PR #13011: Minimal changes to make the refman compatible with Sphinx 3.

Reviewed-by: cpitclaudel
Reviewed-by: jfehrle
Ack-by: Zimmi48

2 files changed, 3 insertions, 6 deletions

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