From 36e38a3768251dbcf20c4de2b746e5eee33da909 Mon Sep 17 00:00:00 2001
From: Clément Pit-Claudel
Date: Fri, 18 May 2018 01:12:10 -0400
Subject: [doc] Use productionlist instead of prodn in ring.rst

---
 doc/sphinx/addendum/ring.rst | 23 +++++++++++------------
 1 file changed, 11 insertions(+), 12 deletions(-)

(limited to 'doc')

diff --git a/doc/sphinx/addendum/ring.rst b/doc/sphinx/addendum/ring.rst
index 47d3a7d7cd..6a9b343ba8 100644
--- a/doc/sphinx/addendum/ring.rst
+++ b/doc/sphinx/addendum/ring.rst
@@ -310,16 +310,15 @@ The :n:`@ident` is not relevant. It is just used for error messages. The
 axioms. The optional list of modifiers is used to tailor the behavior
 of the tactic. The following list describes their syntax and effects:
 
-.. prodn::
-   ring_mod ::= abstract %| decidable @term %| morphism @term
-                %| setoid @term @term 
-                %| constants [@ltac] 
-                %| preprocess [@ltac]
-                %| postprocess [@ltac]
-                %| power_tac @term [@ltac] 
-                %| sign @term
-                %| div @term
-
+.. productionlist:: coq
+   ring_mod : abstract | decidable `term` | morphism `term`
+            : | setoid `term` `term`
+            : | constants [`ltac`]
+            : | preprocess [`ltac`]
+            : | postprocess [`ltac`]
+            : | power_tac `term` [`ltac`]
+            : | sign `term`
+            : | div `term`
 
 abstract
   declares the ring as abstract. This is the default.
@@ -663,8 +662,8 @@ messages. :n:`@term` is a proof that the field signature satisfies the
 (semi-)field axioms. The optional list of modifiers is used to tailor
 the behavior of the tactic.
 
-.. prodn::
-   field_mod := @ring_mod %| completeness @term
+.. productionlist:: coq
+   field_mod : `ring_mod` | completeness `term`
 
 Since field tactics are built upon ``ring``
 tactics, all modifiers of the ``Add Ring`` apply. There is only one
-- 
cgit v1.2.3