More natural notation for intro pattern: @a -> ?a

Caveat about a slight loss of compatibility: 
Some intro patterns don't need space between them. In particular 
intros ?a?b used to be legal and equivalent to intros ? a ? b. Now it
is still legal but equivalent to intros ?a ?b. 



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

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