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/tools/docgram/README.md | 1 -
 1 file changed, 1 deletion(-)

(limited to 'doc/tools/docgram')

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
-- 
cgit v1.2.3