aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/refman/RefMan-syn.tex
diff options
context:
space:
mode:
authorGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2015-01-29 20:04:22 +0100
committerGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2015-01-29 20:04:32 +0100
commitdb293d185f8deb091d4b086f327caa0f376d67d7 (patch)
treea717722126a8e35c5822f0122277553a8507453c /doc/refman/RefMan-syn.tex
parentc0d777549b8796e4d4f542d68fe1be42b772025e (diff)
Fix index of reference manual.
Diffstat (limited to 'doc/refman/RefMan-syn.tex')
-rw-r--r--doc/refman/RefMan-syn.tex2
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/refman/RefMan-syn.tex b/doc/refman/RefMan-syn.tex
index df4066169..11954ed0e 100644
--- a/doc/refman/RefMan-syn.tex
+++ b/doc/refman/RefMan-syn.tex
@@ -878,7 +878,7 @@ interpretation. See the next section.
\SeeAlso The command to show the scopes bound to the arguments of a
function is described in Section~\ref{About}.
-\subsection[The {\tt type\_scope} interpretation scope]{The {\tt type\_scope} interpretation scope\index{type\_scope}}
+\subsection[The {\tt type\_scope} interpretation scope]{The {\tt type\_scope} interpretation scope\index{type\_scope@\texttt{type\_scope}}}
The scope {\tt type\_scope} has a special status. It is a primitive
interpretation scope which is temporarily activated each time a