diff options
Diffstat (limited to 'doc/sphinx/addendum/ring.rst')
| -rw-r--r-- | doc/sphinx/addendum/ring.rst | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/doc/sphinx/addendum/ring.rst b/doc/sphinx/addendum/ring.rst index 99d689132d..8204d93fa7 100644 --- a/doc/sphinx/addendum/ring.rst +++ b/doc/sphinx/addendum/ring.rst @@ -308,13 +308,13 @@ The syntax for adding a new ring is .. 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` + : 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. |