diff options
| author | Jim Fehrle | 2019-12-18 23:23:34 -0800 |
|---|---|---|
| committer | Jim Fehrle | 2019-12-28 12:34:47 -0800 |
| commit | 7b143ed46ab2b1b804b834b59533bef5960be9bc (patch) | |
| tree | 97736e1de02a980f21880f4466009707e71821f8 /doc/sphinx/addendum | |
| parent | bdb5150669d5ac972d3d2b3c9cc2045e77dc9ad5 (diff) | |
Convert productionlists to prodns
Diffstat (limited to 'doc/sphinx/addendum')
| -rw-r--r-- | doc/sphinx/addendum/extended-pattern-matching.rst | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/sphinx/addendum/extended-pattern-matching.rst b/doc/sphinx/addendum/extended-pattern-matching.rst index 45b3f6f161..15f42591ce 100644 --- a/doc/sphinx/addendum/extended-pattern-matching.rst +++ b/doc/sphinx/addendum/extended-pattern-matching.rst @@ -192,7 +192,7 @@ Disjunctive patterns -------------------- Multiple patterns that share the same right-hand-side can be -factorized using the notation :n:`{+| @patterns_comma}`. For +factorized using the notation :n:`{+| {+, @pattern } }`. For instance, :g:`max` can be rewritten as follows: .. coqtop:: in reset |