From 7b143ed46ab2b1b804b834b59533bef5960be9bc Mon Sep 17 00:00:00 2001
From: Jim Fehrle
Date: Wed, 18 Dec 2019 23:23:34 -0800
Subject: Convert productionlists to prodns

---
 doc/sphinx/addendum/extended-pattern-matching.rst | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'doc/sphinx/addendum')

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
-- 
cgit v1.2.3