aboutsummaryrefslogtreecommitdiff
path: root/doc/tools/coqrst/coqdomain.py
diff options
context:
space:
mode:
Diffstat (limited to 'doc/tools/coqrst/coqdomain.py')
-rw-r--r--doc/tools/coqrst/coqdomain.py2
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py
index 1784519f5f..4bdfac7c42 100644
--- a/doc/tools/coqrst/coqdomain.py
+++ b/doc/tools/coqrst/coqdomain.py
@@ -418,7 +418,7 @@ class ProductionObject(CoqObject):
Example::
.. prodn:: term += let: @pattern := @term in @term
- .. prodn:: occ_switch ::= { {? + %| - } {* @num } }
+ .. prodn:: occ_switch ::= { {? {| + | - } } {* @num } }
"""
subdomain = "prodn"