diff options
| author | herbelin | 2005-05-20 16:34:37 +0000 |
|---|---|---|
| committer | herbelin | 2005-05-20 16:34:37 +0000 |
| commit | 308baaeb64bb93af456a88e93f5da14264a95cc6 (patch) | |
| tree | 3d33abf5d96302b18178816d0df680a290961278 | |
| parent | aceda714576e1cbaa12dbf1f12507c8a625934ef (diff) | |
Updated new names of Local into Let
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8602 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rwxr-xr-x | doc/RefMan-pro.tex | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/doc/RefMan-pro.tex b/doc/RefMan-pro.tex index 68f96f7cca..7565612d14 100755 --- a/doc/RefMan-pro.tex +++ b/doc/RefMan-pro.tex @@ -155,8 +155,8 @@ as a {\tt Theorem}, the name {\ident} is known at all section levels: {\tt Defined} (see \ref{Defined}) in order to define a transparent constant. -\item {\tt Local {\ident} : {\form}.} -\comindex{Local} +\item {\tt Let {\ident} : {\form}.} +\comindex{Let} Analogous to {\tt Definition} except that the definition is turned into a local definition on objects depending on it after closing the |