New intro pattern "@A", which generates a fresh name based on A.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9950 85f007b7-540e-0410-9357-904b9bb8a0f7

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