Documentation or-pattern

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9005 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 11 insertions, 7 deletions

diff --git a/doc/refman/RefMan-gal.tex b/doc/refman/RefMan-gal.tex
index c2869fd3da..e80a53f5ba 100644
--- a/doc/refman/RefMan-gal.tex
+++ b/doc/refman/RefMan-gal.tex
@@ -308,7 +308,9 @@ chapter \ref{Addoc-syntax}.
 &&\\
 {\returntype} & ::= & {\tt return} {\term} \\
 &&\\
-{\eqn} & ::= & \nelist{\pattern}{\tt ,} {\tt =>} {\term}\\
+{\eqn} & ::= & \nelist{\multpattern}{\tt |} {\tt =>} {\term}\\
+&&\\
+{\multpattern} & ::= & \nelist{\pattern}{\tt ,}\\
 &&\\
 {\pattern} & ::= & {\qualid} \nelist{\pattern}{}  \\
  & $|$ & {\pattern} {\tt as} {\ident}             \\
@@ -316,7 +318,9 @@ chapter \ref{Addoc-syntax}.
  & $|$ & {\qualid}                              \\
  & $|$ & {\tt \_}                                  \\
  & $|$ & {\num}                                 \\
- & $|$ & {\tt (} \nelist{\pattern}{,} {\tt )}     
+ & $|$ & {\tt (} \nelist{\orpattern}{,} {\tt )}     \\
+\\
+{\orpattern} & ::= & \nelist{\pattern}{\tt |}\\
 \end{tabular}
 \end{centerframe}
 \caption{Syntax of terms (continued)}
@@ -515,10 +519,11 @@ The expression {\tt match} {\term$_0$} {\returntype} {\tt with}
 {\pattern$_1$} {\tt =>} {\term$_1$} {\tt $|$} {\ldots} {\tt $|$}
 {\pattern$_n$} {\tt =>} {\term$_n$} {\tt end}, denotes a {\em
 pattern-matching} over the term {\term$_0$} (expected to be of an
-inductive type $I$). {\term$_1$}\ldots{\term$_n$} are called branches. In
+inductive type $I$). 
+The terms {\term$_1$}\ldots{\term$_n$} are called branches. In
 a simple pattern \qualid~\nelist{\ident}{}, the qualified identifier
 {\qualid} is intended to
-be a constructor. There should be a branch for every constructor of
+be a constructor. There should be one branch for every constructor of
 $I$.
 
 The {\returntype} is used to compute the resulting type of the whole
@@ -530,9 +535,8 @@ annotation has to be given when the resulting type of the whole {\tt
 match} depends on the actual {\term$_0$} matched.
 
 There are specific notations for case analysis on types with one or
-two constructors: {\tt if / then / else} and
-{\tt let (}\ldots{\tt ) :=} \ldots {\tt in}\ldots. \SeeAlso
-section~\ref{Mult-match} for details and examples.
+two constructors: {\tt if {\ldots} then {\ldots} else {\ldots}} and
+{\tt let (}\nelist{\ldots}{,}{\tt ) :=} {\ldots} {\tt in} {\ldots}.
 
 \SeeAlso Section~\ref{Mult-match} for details and examples.