diff options
Diffstat (limited to 'doc/refman')
| -rw-r--r-- | doc/refman/RefMan-tac.tex | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index 8dd168aad..864a004fe 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -1451,7 +1451,7 @@ An introduction pattern is either: \begin{itemize} \item the wildcard: {\tt \_} \item the pattern \texttt{?} -\item the pattern \texttt{@\ident} +\item the pattern \texttt{?\ident} \item a variable \item a disjunction of lists of patterns: {\tt [$p_{11}$ {\ldots} $p_{1m_1}$ | {\ldots} | $p_{11}$ {\ldots} $p_{nm_n}$]} @@ -1465,7 +1465,7 @@ structure of the pattern given as argument: immediately clear (cf~\ref{clear}) the corresponding hypothesis; \item introduction on \texttt{?} do the introduction, and let Coq choose a fresh name for the variable; -\item introduction on \texttt{@\ident} do the introduction, and let Coq +\item introduction on \texttt{?\ident} do the introduction, and let Coq choose a fresh name for the variable based on {\ident}; \item introduction on a variable behaves like described in~\ref{intro}; \item introduction over a |