diff options
| -rw-r--r-- | doc/RefMan-ext.tex | 2 | ||||
| -rwxr-xr-x | doc/RefMan-syn.tex | 4 |
2 files changed, 3 insertions, 3 deletions
diff --git a/doc/RefMan-ext.tex b/doc/RefMan-ext.tex index 55b4e71ad8..9f66c2850b 100644 --- a/doc/RefMan-ext.tex +++ b/doc/RefMan-ext.tex @@ -920,7 +920,7 @@ Conversely, use command {\tt Unset Contextual Implicit} to unset the contextual implicit mode. \subsection{Explicit Applications} -\comindex{Explicitation of implicit arguments} +\index{Explicitation of implicit arguments} \label{Implicits-explicitation} \index{@{\qualid}} 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 |