diff options
| author | Maxime Dénès | 2018-06-21 17:40:13 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2018-06-21 17:40:13 +0200 |
| commit | 41cf6afdb70b073838bd2a1e71f76c600e03c006 (patch) | |
| tree | ac599113aa91feef19fa1d59feeaa27a685ce360 /doc/sphinx/addendum | |
| parent | be6f66e3d4424b0dfbbbe3097a617aebb8aefca2 (diff) | |
| parent | 3d8342c2c26f710583e6b9246bd1069cb8b42d7d (diff) | |
Merge PR #7865: Fix #7432: Grammar token @term points to the SSR chapter.
Diffstat (limited to 'doc/sphinx/addendum')
| -rw-r--r-- | doc/sphinx/addendum/ring.rst | 23 |
1 files changed, 11 insertions, 12 deletions
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 |