[doc] Rewrite and document the prodn directive

It was broken and undocumented. We dropped the git logs, too, so it wasn't clear
who wrote it and why it was introduced in the first place.

1 files changed, 14 insertions, 1 deletions

diff --git a/doc/sphinx/README.rst b/doc/sphinx/README.rst
index 35a605ddd..32de15ee3 100644
--- a/doc/sphinx/README.rst
+++ b/doc/sphinx/README.rst
@@ -123,11 +123,24 @@ Here is the list of all objects of the Coq domain (The symbol :black_nib: indica
           :cmd:`Variant` and :cmd:`Record` get an automatic declaration of the
           induction principles.
 
-``.. prodn::`` :black_nib: Grammar productions.
+``.. prodn::`` A grammar production.
     This is useful if you intend to document individual grammar productions.
     Otherwise, use Sphinx's `production lists
     <http://www.sphinx-doc.org/en/stable/markup/para.html#directive-productionlist>`_.
 
+    Unlike ``.. productionlist``\ s, this directive accepts notation syntax.
+
+
+    Usage::
+
+       .. prodn:: token += production
+       .. prodn:: token ::= production
+
+    Example::
+
+        .. prodn:: term += let: @pattern := @term in @term
+        .. prodn:: occ_switch ::= { {? + %| - } {* @num } }
+
 ``.. tacn::`` :black_nib: A tactic, or a tactic notation.
     Example::