diff options
| author |  pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-02-29 13:33:24 +0000 |
|---|---|---|
| committer | pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-02-29 13:33:24 +0000 |
| commit | 457bf8fee3b53b8306d0dcdf49e637c29592d6c3 (patch) | |
| tree | 76d5c06746bae78c165971732cc5f2b7304484b0 /doc/refman/RefMan-gal.tex | |
| parent | e51161ffec1a5ef34bf19394f5554b86b39e24bb (diff) | |
RefMan update about match syntax.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15002 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'doc/refman/RefMan-gal.tex')
| -rw-r--r-- | doc/refman/RefMan-gal.tex | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/doc/refman/RefMan-gal.tex b/doc/refman/RefMan-gal.tex index 6fe9c08d3..45f0dce21 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} \term} \\ + \zeroone{{\tt in} \pattern} \\ &&\\ {\ifitem} & ::= & \zeroone{{\tt as} {\name}} {\returntype} \\ &&\\ @@ -322,6 +322,8 @@ called \CIC). The formal presentation of {\CIC} is given in Chapter {\multpattern} & ::= & \nelist{\pattern}{\tt ,}\\ &&\\ {\pattern} & ::= & {\qualid} \nelist{\pattern}{} \\ + & $|$ & {\tt @} {\qualid} \sequence{\pattern}{} \\ + & $|$ & {\pattern} {\tt as} {\ident} \\ & $|$ & {\pattern} {\tt \%} {\ident} \\ & $|$ & {\qualid} \\ |