From 3d8342c2c26f710583e6b9246bd1069cb8b42d7d Mon Sep 17 00:00:00 2001 From: Clément Pit-Claudel Date: Fri, 18 May 2018 01:10:15 -0400 Subject: [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. --- doc/sphinx/README.rst | 15 ++++++++++++++- 1 file changed, 14 insertions(+), 1 deletion(-) (limited to 'doc/sphinx') 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 `_. + 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:: -- cgit v1.2.3