diff options
Diffstat (limited to 'doc/refman/RefMan-ext.tex')
| -rw-r--r-- | doc/refman/RefMan-ext.tex | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex index 193479cce..3605a716e 100644 --- a/doc/refman/RefMan-ext.tex +++ b/doc/refman/RefMan-ext.tex @@ -167,7 +167,7 @@ defined with the {\tt Record} keyword can be activated with the (see~\ref{set-nonrecursive-elimination-schemes}). \begin{Warnings} -\item {\tt Warning: {\ident$_i$} cannot be defined.} +\item {\tt {\ident$_i$} cannot be defined.} It can happen that the definition of a projection is impossible. This message is followed by an explanation of this impossibility. @@ -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}}} |