diff options
| author | herbelin | 2004-04-02 17:09:44 +0000 |
|---|---|---|
| committer | herbelin | 2004-04-02 17:09:44 +0000 |
| commit | e449068f3de2ce2efcc8798a87394cd6428b0775 (patch) | |
| tree | 8859a97323cddf463af5294b569d31b97741f378 /doc | |
| parent | 62bbd0d2bc33d53ec4c46b424de0587eaca7c1d6 (diff) | |
Bug {\ifitem}
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8529 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/RefMan-gal.tex | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/doc/RefMan-gal.tex b/doc/RefMan-gal.tex index 0696f17020..a73f4f18a3 100644 --- a/doc/RefMan-gal.tex +++ b/doc/RefMan-gal.tex @@ -228,10 +228,10 @@ chapter \ref{Addoc-syntax}. & $|$ & {\tt let fix} {\fixpointbody} {\tt in} {\term} &(\ref{fixpoints})\\ & $|$ & {\tt let cofix} {\cofixpointbody} {\tt in} {\term} &(\ref{fixpoints})\\ - & $|$ & {\tt let} {\tt (} \sequence{\name}{,} {\tt )} {\ifitem} + & $|$ & {\tt let} {\tt (} \sequence{\name}{,} {\tt )} \zeroone{\ifitem} {\tt :=} {\term} {\tt in} {\term} &(\ref{caseanalysis}, \ref{Mult-match})\\ - & $|$ & {\tt if} {\term} {\ifitem} {\tt then} {\term} + & $|$ & {\tt if} {\term} \zeroone{\ifitem} {\tt then} {\term} {\tt else} {\term} &(\ref{caseanalysis}, \ref{Mult-match})\\ & $|$ & {\term} {\tt :} {\term} &(\ref{typecast})\\ & $|$ & {\term} {\tt ->} {\term} &(\ref{products})\\ @@ -304,7 +304,7 @@ chapter \ref{Addoc-syntax}. {\caseitem} & ::= & {\term} \zeroone{{\tt as} \name} \zeroone{{\tt in} \term} \\ &&\\ -{\ifitem} & ::= & {\term} \zeroone{\zeroone{{\tt as} {\name}} {\returntype}} \\ +{\ifitem} & ::= & \zeroone{{\tt as} {\name}} {\returntype} \\ &&\\ {\returntype} & ::= & {\tt return} {\term} \\ &&\\ |