diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/refman/RefMan-tac.tex | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index dc2f65a152..d04d8e3134 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -1442,6 +1442,7 @@ An introduction pattern is either: \begin{itemize} \item the wildcard: {\tt \_} \item the pattern \texttt{?} +\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}$]} @@ -1455,6 +1456,8 @@ 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 + 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 list of patterns $p_1~\ldots~p_n$ is equivalent to the sequence of |