From cdd37b4a3d29e85c0538833b06ceac2140fa4ecc Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Wed, 14 Jan 2015 14:50:31 +0100
Subject: Reference manual: I had previously omitted the syntax entry for [>
 t1|…|tn].

---
 doc/refman/RefMan-ltac.tex | 1 +
 1 file changed, 1 insertion(+)

diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex
index 73bcc85871..b90e682df1 100644
--- a/doc/refman/RefMan-ltac.tex
+++ b/doc/refman/RefMan-ltac.tex
@@ -91,6 +91,7 @@ is understood as
 \begin{tabular}{lcl}
 {\tacexpr} & ::= &
            {\tacexpr} {\tt ;} {\tacexpr}\\
+& | & {\tt [>} \nelist{\tacexpr}{|} {\tt ]}\\
 & | & {\tacexpr} {\tt ; [} \nelist{\tacexpr}{|} {\tt ]}\\
 & | & {\tacexprpref}\\
 \\
-- 
cgit v1.2.3