Fix index of reference manual.

6 files changed, 57 insertions, 52 deletions

diff --git a/doc/refman/RefMan-com.tex b/doc/refman/RefMan-com.tex
index a93733256..49bcdb1db 100644
--- a/doc/refman/RefMan-com.tex
+++ b/doc/refman/RefMan-com.tex
@@ -1,6 +1,7 @@
 \chapter[The \Coq~commands]{The \Coq~commands\label{Addoc-coqc}
 \ttindex{coqtop}
-\ttindex{coqc}}
+\ttindex{coqc}
+\ttindex{coqchk}}
 
 There are three \Coq~commands: 
 \begin{itemize}
diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex
index 4b197ec73..3605a716e 100644
--- a/doc/refman/RefMan-ext.tex
+++ b/doc/refman/RefMan-ext.tex
@@ -434,7 +434,7 @@ we have an equivalence between
 {\tt match {\term} \zeroone{\ifitem} with C {\ident}$_1$ {\ldots} {\ident}$_n$ \verb!=>! {\term}' end}
 
 
-\subsubsection{Second destructuring {\tt let} syntax\index{let '... in}}
+\subsubsection{Second destructuring {\tt let} syntax\index{let '... in@\texttt{let '... in}}}
 
 Another destructuring {\tt let} syntax is available for inductive types with
 one constructor by giving an arbitrary pattern instead of just a tuple
@@ -2000,7 +2000,7 @@ variables, use
 \end{quote}
 
 \subsection{Solving existential variables using tactics}
-\index{\tt \textdollar( \ldots )\textdollar}
+\ttindex{\textdollar( \ldots )\textdollar}
 
 \def\expr{\textrm{\textsl{tacexpr}}}
 
diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex
index de8c26943..689ac1425 100644
--- a/doc/refman/RefMan-ltac.tex
+++ b/doc/refman/RefMan-ltac.tex
@@ -620,10 +620,10 @@ runs is displayed. Time is in seconds and is machine-dependent. The
 {\qstring} argument is optional. When provided, it is used to identify
 this particular occurrence of {\tt time}.
 
-\subsubsection[Local definitions]{Local definitions\index{Ltac!let}
-\index{Ltac!let rec}
-\index{let!in Ltac}
-\index{let rec!in Ltac}}
+\subsubsection[Local definitions]{Local definitions\index{Ltac!let@\texttt{let}}
+\index{Ltac!let rec@\texttt{let rec}}
+\index{let@\texttt{let}!in Ltac}
+\index{let rec@\texttt{let rec}!in Ltac}}
 
 Local definitions can be done as follows:
 \begin{quote}
@@ -659,8 +659,8 @@ definition expecting at least $n$ arguments.  The expressions
 
 %\subsection{Application of tactic values}
 
-\subsubsection[Function construction]{Function construction\index{fun!in Ltac}
-\index{Ltac!fun}}
+\subsubsection[Function construction]{Function construction\index{fun@\texttt{fun}!in Ltac}
+\index{Ltac!fun@\texttt{fun}}}
 
 A parameterized tactic can be built anonymously (without resorting to
 local definitions) with:
@@ -670,8 +670,8 @@ local definitions) with:
 Indeed, local definitions of functions are a syntactic sugar for
 binding a {\tt fun} tactic to an identifier.
 
-\subsubsection[Pattern matching on terms]{Pattern matching on terms\index{Ltac!match}
-\index{match!in Ltac}}
+\subsubsection[Pattern matching on terms]{Pattern matching on terms\index{Ltac!match@\texttt{match}}
+\index{match@\texttt{match}!in Ltac}}
 
 We can carry out pattern matching on terms with:
 \begin{quote}
@@ -729,8 +729,8 @@ it has backtracking points.
 
 \begin{Variants}
 
-\item \index{multimatch!in Ltac}
-\index{Ltac!multimatch}
+\item \index{multimatch@\texttt{multimatch}!in Ltac}
+\index{Ltac!multimatch@\texttt{multimatch}}
 Using {\tt multimatch} instead of {\tt match} will allow subsequent
 tactics to backtrack into a right-hand side tactic which has
 backtracking points left and trigger the selection of a new matching
@@ -740,8 +740,8 @@ been consumed.
 The syntax {\tt match \ldots} is, in fact, a shorthand for
 {\tt once multimatch \ldots}.
 
-\item \index{lazymatch!in Ltac}
-\index{Ltac!lazymatch}
+\item \index{lazymatch@\texttt{lazymatch}!in Ltac}
+\index{Ltac!lazymatch@\texttt{lazymatch}}
 Using {\tt lazymatch} instead of {\tt match} will perform the same
 pattern matching procedure but will commit to the first matching
 branch rather than trying a new matching if the right-hand side
@@ -749,7 +749,7 @@ fails. If the right-hand side of the selected branch is a tactic with
 backtracking points, then subsequent failures cause this tactic to
 backtrack.
 
-\item \index{context!in pattern}
+\item \index{context@\texttt{context}!in pattern}
 There is a special form of patterns to match a subterm against the
 pattern:
 \begin{quote}
@@ -778,7 +778,7 @@ Goal True.
 f (3+4).
 \end{coq_example}
 
-\item \index{appcontext!in pattern}
+\item \index{appcontext@\texttt{appcontext}!in pattern}
   \comindex{Set Tactic Compat Context}
   \comindex{Unset Tactic Compat Context}
 For historical reasons, {\tt context} used to consider $n$-ary applications
@@ -796,10 +796,10 @@ behavior can be retrieved with the {\tt Tactic Compat Context} flag.
 
 \end{Variants}
 
-\subsubsection[Pattern matching on goals]{Pattern matching on goals\index{Ltac!match goal}
-\index{Ltac!match reverse goal}
-\index{match goal!in Ltac}
-\index{match reverse goal!in Ltac}}
+\subsubsection[Pattern matching on goals]{Pattern matching on goals\index{Ltac!match goal@\texttt{match goal}}
+\index{Ltac!match reverse goal@\texttt{match reverse goal}}
+\index{match goal@\texttt{match goal}!in Ltac}
+\index{match reverse goal@\texttt{match reverse goal}!in Ltac}}
 
 We can make pattern matching on goals using the following expression:
 \begin{quote}
@@ -854,10 +854,10 @@ the {\tt match reverse goal with} variant.
 
 \variant
 
-\index{multimatch goal!in Ltac}
-\index{Ltac!multimatch goal}
-\index{multimatch reverse goal!in Ltac}
-\index{Ltac!multimatch reverse goal}
+\index{multimatch goal@\texttt{multimatch goal}!in Ltac}
+\index{Ltac!multimatch goal@\texttt{multimatch goal}}
+\index{multimatch reverse goal@\texttt{multimatch reverse goal}!in Ltac}
+\index{Ltac!multimatch reverse goal@\texttt{multimatch reverse goal}}
 
 Using {\tt multimatch} instead of {\tt match} will allow subsequent
 tactics to backtrack into a right-hand side tactic which has
@@ -868,10 +868,10 @@ of the right-hand side have been consumed.
 The syntax {\tt match [reverse] goal \ldots} is, in fact, a shorthand for
 {\tt once multimatch [reverse] goal \ldots}.
 
-\index{lazymatch goal!in Ltac}
-\index{Ltac!lazymatch goal}
-\index{lazymatch reverse goal!in Ltac}
-\index{Ltac!lazymatch reverse goal}
+\index{lazymatch goal@\texttt{lazymatch goal}!in Ltac}
+\index{Ltac!lazymatch goal@\texttt{lazymatch goal}}
+\index{lazymatch reverse goal@\texttt{lazymatch reverse goal}!in Ltac}
+\index{Ltac!lazymatch reverse goal@\texttt{lazymatch reverse goal}}
 Using {\tt lazymatch} instead of {\tt match} will perform the same
 pattern matching procedure but will commit to the first matching
 branch with the first matching combination of hypotheses rather than
@@ -879,7 +879,7 @@ trying a new matching if the right-hand side fails. If the right-hand
 side of the selected branch is a tactic with backtracking points, then
 subsequent failures cause this tactic to backtrack.
 
-\subsubsection[Filling a term context]{Filling a term context\index{context!in expression}}
+\subsubsection[Filling a term context]{Filling a term context\index{context@\texttt{context}!in expression}}
 
 The following expression is not a tactic in the sense that it does not
 produce subgoals but generates a term to be used in tactic
@@ -895,8 +895,8 @@ replaces the hole of the value of {\ident} by the value of
 \ErrMsg \errindex{not a context variable}
 
 
-\subsubsection[Generating fresh hypothesis names]{Generating fresh hypothesis names\index{Ltac!fresh}
-\index{fresh!in Ltac}}
+\subsubsection[Generating fresh hypothesis names]{Generating fresh hypothesis names\index{Ltac!fresh@\texttt{fresh}}
+\index{fresh@\texttt{fresh}!in Ltac}}
 
 Tactics sometimes have to generate new names for hypothesis. Letting
 the system decide a name with the {\tt intro} tactic is not so good
@@ -913,8 +913,8 @@ has to refer to a name, or directly a name denoted by a
 with a number so that it becomes fresh. If no component is
 given, the name is a fresh derivative of the name {\tt H}.
 
-\subsubsection[Computing in a constr]{Computing in a constr\index{Ltac!eval}
-\index{eval!in Ltac}}
+\subsubsection[Computing in a constr]{Computing in a constr\index{Ltac!eval@\texttt{eval}}
+\index{eval@\texttt{eval}!in Ltac}}
 
 Evaluation of a term can be performed with:
 \begin{quote}
@@ -926,8 +926,8 @@ hnf}, {\tt compute}, {\tt simpl}, {\tt cbv}, {\tt lazy}, {\tt unfold},
 
 \subsubsection{Recovering the type of a term}
 %\tacindex{type of}
-\index{Ltac!type of}
-\index{type of!in Ltac}
+\index{Ltac!type of@\texttt{type of}}
+\index{type of@\texttt{type of}!in Ltac}
 
 The following returns the type of {\term}:
 
@@ -935,7 +935,10 @@ The following returns the type of {\term}:
 {\tt type of} {\term}
 \end{quote}
 
-\subsubsection[Manipulating untyped terms]{Manipulating untyped terms\index{Ltac!uconstr}\index{uconstr!in Ltac}\index{Ltac!type\_term}\index{type\_term!in Ltac}}
+\subsubsection[Manipulating untyped terms]{Manipulating untyped terms\index{Ltac!uconstr@\texttt{uconstr}}
+\index{uconstr@\texttt{uconstr}!in Ltac}
+\index{Ltac!type\_term@\texttt{type\_term}}
+\index{type\_term@\texttt{type\_term}!in Ltac}}
 
 The terms built in Ltac are well-typed by default. It may not be
 appropriate for building large terms using a recursive Ltac function:
@@ -963,7 +966,7 @@ untyped term is type checked against the conclusion of the goal, and
 the holes which are not solved by the typing procedure are turned into
 new subgoals.
 
-\subsubsection[Counting the goals]{Counting the goals\index{Ltac!numgoals}\index{numgoals!in Ltac}}
+\subsubsection[Counting the goals]{Counting the goals\index{Ltac!numgoals@\texttt{numgoals}}\index{numgoals@\texttt{numgoals}!in Ltac}}
 
 The number of goals under focus can be recovered using the {\tt
   numgoals} function. Combined with the {\tt guard} command below, it
@@ -979,7 +982,7 @@ split;[|split].
 all:pr_numgoals.
 \end{coq_example}
 
-\subsubsection[Testing boolean expressions]{Testing boolean expressions\index{Ltac!guard}\index{guard!in Ltac}}
+\subsubsection[Testing boolean expressions]{Testing boolean expressions\index{Ltac!guard@\texttt{guard}}\index{guard@\texttt{guard}!in Ltac}}
 
 The {\tt guard} tactic tests a boolean expression, and fails if the expression evaluates to false. If the expression evaluates to true, it succeeds without affecting the proof.
 
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
diff --git a/doc/refman/RefMan-uti.tex b/doc/refman/RefMan-uti.tex
index 07d711424..48e2df19d 100644
--- a/doc/refman/RefMan-uti.tex
+++ b/doc/refman/RefMan-uti.tex
@@ -3,7 +3,7 @@
 The distribution provides utilities to simplify some tedious works
 beside proof development, tactics writing or documentation.
 
-\section[Building a toplevel extended with user tactics]{Building a toplevel extended with user tactics\label{Coqmktop}\index{Coqmktop@{\tt coqmktop}}}
+\section[Building a toplevel extended with user tactics]{Building a toplevel extended with user tactics\label{Coqmktop}\ttindex{coqmktop}}
 
 The native-code version of \Coq\ cannot dynamically load user tactics
 using {\ocaml} code. It is possible to build a toplevel of \Coq,
@@ -52,7 +52,7 @@ arguments. Such a wrapper can be found in the \texttt{dev/}
 subdirectory of the sources. 
 
 \section[Modules dependencies]{Modules dependencies\label{Dependencies}\index{Dependencies}
-  \index{Coqdep@{\tt coqdep}}}
+  \ttindex{coqdep}}
 
 In order to compute modules dependencies (so to use {\tt make}),
 \Coq\ comes with an appropriate tool, {\tt coqdep}.
@@ -75,8 +75,8 @@ See the man page of {\tt coqdep} for more details and options.
 
 
 \section[Creating a {\tt Makefile} for \Coq\ modules]{Creating a {\tt Makefile} for \Coq\ modules\label{Makefile}
-\index{Makefile@{\tt Makefile}}
-\index{CoqMakefile@{\tt coq\_Makefile}}}
+\ttindex{Makefile}
+\ttindex{coq\_Makefile}}
 
 \paragraph{\_CoqProject}
 When a proof development becomes a larger project, split into several
@@ -128,8 +128,8 @@ will recursively call this target in all the subdirectories.
   dependencies on already defined rules. For example the following
   skeleton appends something to the \texttt{install} rule:
 \begin{quotation}
-\texttt{-extra-phony ``install'' ``install-my-stuff'' ``''
-  -extra-phony ``install-my-stuff'' ``'' ``something''}
+\texttt{-extra-phony "install" "install-my-stuff" ""
+  -extra-phony "install-my-stuff" "" "something"}
 \end{quotation}
 \end{itemize}
 
@@ -146,12 +146,12 @@ to generate a \texttt{Makefile} the first time. \texttt{Makefile} will be
 automatically regenerated when \texttt{\_CoqProject} is updated afterward.
 
 \section[Documenting \Coq\ files with coqdoc]{Documenting \Coq\ files with coqdoc\label{coqdoc}
-\index{Coqdoc@{\sf coqdoc}}}
+\ttindex{coqdoc}}
 
 \input{./coqdoc}
 
 \section[Embedded \Coq\ phrases inside \LaTeX\ documents]{Embedded \Coq\ phrases inside \LaTeX\ documents\label{Latex}
-  \index{Coqtex@{\tt coq-tex}}\index{Latex@{\LaTeX}}}
+  \ttindex{coq-tex}\index{Latex@{\LaTeX}}}
 
 When writing a documentation about a proof development, one may want
 to insert \Coq\ phrases inside a \LaTeX\ document, possibly together with
@@ -207,7 +207,7 @@ An inferior mode to run \Coq\ under Emacs, by Marco Maggesi, is also
 included in the distribution, in file \texttt{coq-inferior.el}.
 Instructions to use it are contained in this file.
 
-\subsection[{\ProofGeneral}]{{\ProofGeneral}\index{\ProofGeneral}}
+\subsection[{\ProofGeneral}]{{\ProofGeneral}\index{Proof General@{\ProofGeneral}}}
 
 {\ProofGeneral} is a generic interface for proof assistants based on
 Emacs. The main idea is that the \Coq\ commands you are
@@ -221,7 +221,7 @@ files.
 system \Coq. It is freely available at \verb!proofgeneral.inf.ed.ac.uk!.
 
 
-\section[Module specification]{Module specification\label{gallina}\index{Gallina@{\tt gallina}}}
+\section[Module specification]{Module specification\label{gallina}\ttindex{gallina}}
 
 Given a \Coq\ vernacular file, the {\tt gallina} filter extracts its
 specification (inductive types declarations, definitions, type of
diff --git a/doc/refman/coqdoc.tex b/doc/refman/coqdoc.tex
index b66cbb436..b42480a56 100644
--- a/doc/refman/coqdoc.tex
+++ b/doc/refman/coqdoc.tex
@@ -252,8 +252,9 @@ suffix \verb!.tex!.
 
 \item[\texmacs\ output] ~\par
   To translate the input files to \texmacs\ format, to be used by
-  the \texmacs\ Coq interface 
-  (see \url{http://www-sop.inria.fr/lemme/Philippe.Audebaud/tmcoq/}).
+  the \texmacs\ Coq interface.
+  %broken link:
+  %(see \url{http://www-sop.inria.fr/lemme/Philippe.Audebaud/tmcoq/}).
 \end{description}