RefMan, ch. 4: Reference Manual: more on the "in pattern" clause and

"@qualid pattern".

2 files changed, 15 insertions, 10 deletions

diff --git a/doc/refman/Cases.tex b/doc/refman/Cases.tex
index 4238bf6a57..a95d8114ff 100644
--- a/doc/refman/Cases.tex
+++ b/doc/refman/Cases.tex
@@ -521,6 +521,8 @@ I have a copy of {\tt b} in type {\tt listn 0} resp {\tt listn (S n')}.
 % \end{coq_example}
 
 \paragraph{Patterns in {\tt in}}
+\label{match-in-patterns}
+
 If the type of the matched term is more precise than an inductive applied to
 variables, arguments of the inductive in the {\tt in} branch can be more
 complicated patterns than a variable.
@@ -530,7 +532,7 @@ become impossible branches. In an impossible branch, you can answer
 anything but {\tt False\_rect unit} has the advantage to be subterm of
 anything. % ???
 
-To be concrete: the tail function can be written:
+To be concrete: the {\tt tail} function can be written:
 \begin{coq_example}
 Definition tail n (v: listn (S n)) :=
   match v in listn (S m) return listn m with
diff --git a/doc/refman/RefMan-gal.tex b/doc/refman/RefMan-gal.tex
index e49c82d8fd..f631c3717c 100644
--- a/doc/refman/RefMan-gal.tex
+++ b/doc/refman/RefMan-gal.tex
@@ -311,7 +311,7 @@ called \CIC). The formal presentation of {\CIC} is given in Chapter
 {\annotation} & ::= & {\tt \{ struct} {\ident} {\tt \}} \\ 
 &&\\
 {\caseitem} & ::= & {\term} \zeroone{{\tt as} \name}
-     \zeroone{{\tt in} \pattern} \\
+     \zeroone{{\tt in} \qualid \sequence{\pattern}{}} \\
 &&\\
 {\ifitem} & ::= & \zeroone{{\tt as} {\name}} {\returntype} \\
 &&\\
@@ -322,7 +322,7 @@ called \CIC). The formal presentation of {\CIC} is given in Chapter
 {\multpattern} & ::= & \nelist{\pattern}{\tt ,}\\
 &&\\
 {\pattern} & ::= & {\qualid} \nelist{\pattern}{}  \\
- & $|$ & {\tt @} {\qualid} \sequence{\pattern}{} \\
+ & $|$ & {\tt @} {\qualid} \nelist{\pattern}{} \\
 
  & $|$ & {\pattern} {\tt as} {\ident}             \\
  & $|$ & {\pattern} {\tt \%} {\ident}         \\
@@ -609,17 +609,20 @@ the type of each branch can depend on the type dependencies specific
 to the branch and the whole pattern-matching expression has a type
 determined by the specific dependencies in the type of the term being
 matched. This dependency of the return type in the annotations of the
-inductive type is expressed using a {\tt
-``in~I~\_~$\ldots$~\_~\ident$_1$~$\ldots$~\ident$_n$}'' clause, where
+inductive type is expressed using a 
+  ``in~I~\_~$\ldots$~\_~\pattern$_1$~$\ldots$~\pattern$_n$'' clause, where
 \begin{itemize}
 \item $I$ is the inductive type of the term being matched;
 
-\item the names \ident$_i$'s correspond to the arguments of the
-inductive type that carry the annotations: the return type is dependent
-on them;
-
-\item the {\_}'s denote the family parameters of the inductive type:
+\item the {\_}'s are matching the parameters of the inductive type:
 the return type is not dependent on them.
+
+\item the \pattern$_i$'s are matching the annotations of the inductive
+  type: the return type is dependent on them
+
+\item in the basic case which we describe below, each \pattern$_i$ is a
+  name \ident$_i$; see \ref{match-in-patterns} for the general case
+
 \end{itemize}
 
 For instance, in the following example: