diff options
| author | Pierre-Marie Pédrot | 2015-01-29 22:40:58 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-01-29 22:40:58 +0100 |
| commit | a340265c9f88df990649481c8ecbe8a513ac4756 (patch) | |
| tree | c9e02defb10bcdb258d75cb6f156657654f65f1f /doc/refman/RefMan-ext.tex | |
| parent | 51b15993cb4a9cc2521b6107b7f4195b21040087 (diff) | |
| parent | db293d185f8deb091d4b086f327caa0f376d67d7 (diff) | |
Merge branch 'v8.5'
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 193479cceb..3605a716e7 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}}} |