From 885aec961ab1a9e3c0c0bfde25742c2a43fddbc5 Mon Sep 17 00:00:00 2001 From: glondu Date: Mon, 9 Jul 2007 15:10:16 +0000 Subject: 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 --- doc/refman/RefMan-tac.tex | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'doc/refman') 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 -- cgit v1.2.3