diff options
| author | marche | 2003-12-09 09:47:24 +0000 |
|---|---|---|
| committer | marche | 2003-12-09 09:47:24 +0000 |
| commit | e31e599f5cd5e539987c2741fece8bb9474dbbc6 (patch) | |
| tree | 5db23aa3818352bc0d097b549c0ccfe46865ec36 /doc/RefMan-syn.tex | |
| parent | d0f3769e208d1ae48b39e07f52fb7a97ba31c8fe (diff) | |
index commands
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8380 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'doc/RefMan-syn.tex')
| -rwxr-xr-x | doc/RefMan-syn.tex | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/doc/RefMan-syn.tex b/doc/RefMan-syn.tex index fbc486fc2e..78ba6cc92b 100755 --- a/doc/RefMan-syn.tex +++ b/doc/RefMan-syn.tex @@ -425,7 +425,7 @@ Locate "'exists' _ | _". % Print Scopes \section{Abbreviations} -\comindex{Abbreviations} +\index{Abbreviations} \label{Abbreviations} An {\em abbreviation} is a name denoting a (presumably) more complex @@ -467,7 +467,7 @@ Abbreviations do not survive the end of sections. No typing of the denoted expression is performed at definition time. Type-checking is done only at the time of use of the abbreviation. -\Rem \comindex{Syntactic Definition (cf Abbreviations)} % For +\Rem \index{Syntactic Definition} % For compatibility Abbreviations are similar to the {\em syntactic definitions} available in versions of {\Coq} prior to version 8.0, except that abbreviations are used for printing (unless the modifier |