From e449068f3de2ce2efcc8798a87394cd6428b0775 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 2 Apr 2004 17:09:44 +0000
Subject: Bug {\ifitem}

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8529 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 doc/RefMan-gal.tex | 6 +++---
 1 file 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} \\
 &&\\
-- 
cgit v1.2.3