From 1bf6166b5e4247e18602ac2967a919fbc02403b4 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 10 Apr 2001 03:09:58 +0000
Subject: typo

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8184 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 doc/RefMan-gal.tex | 10 +++++++++-
 1 file changed, 9 insertions(+), 1 deletion(-)

diff --git a/doc/RefMan-gal.tex b/doc/RefMan-gal.tex
index b38a589d02..9a1da4bd38 100644
--- a/doc/RefMan-gal.tex
+++ b/doc/RefMan-gal.tex
@@ -380,6 +380,7 @@ abstraction when they can be synthetized by the system.
 assumptions. Obviously, this is expanded into unary abstractions
 separated by let-in's.
 
+
 \subsection{Products}
 \index{products}
 
@@ -416,7 +417,14 @@ associativity is to the left.
 binding of \term$_1$ to the variable $\ident$ in \term$_2$.
 
 \medskip
-Rem The expression {\tt [}{\ident}{\tt :=}{\term$_1$}{\tt :}{\type}{\tt ]}{\term$_2$} is equivalent to {\tt [}{\ident}{\tt :=(}{\term$_1$}{\tt ::}{\type}{\tt )]}{\term$_2$}.
+\Rem The expression {\tt [}{\ident}{\tt :=}{\term$_1$}{\tt
+:}{\type}{\tt ]}{\term$_2$} is equivalent to {\tt [}{\ident}{\tt
+:=(}{\term$_1$}{\tt ::}{\type}{\tt )]}{\term$_2$}.
+
+\Rem An alternative equivalent syntax for let-in is {\tt let} {\ident}
+{\tt =} {\term} {\tt in} {\term}.  For historical reasons, the syntax
+{\tt [} {\ident} {\tt =} {\term} {\tt ]} {\term} is also available but
+is not recommended.
 
 \subsection{Definition by case analysis}
 \index{Cases@{\tt Cases\ldots of\ldots end}}
-- 
cgit v1.2.3