diff options
| author |  glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-07-09 15:10:16 +0000 |
|---|---|---|
| committer | glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-07-09 15:10:16 +0000 |
| commit | 885aec961ab1a9e3c0c0bfde25742c2a43fddbc5 (patch) | |
| tree | 83a84ea0935288420121e34a09036ee517b7875d /doc | |
| parent | 9c4f65ebe124d972ae1506e388bb206cb7298ce4 (diff) | |
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
Diffstat (limited to 'doc')
| -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 |