From 627affed266840b4888e7896c2e7fc286a2aab6f Mon Sep 17 00:00:00 2001
From: glondu
Date: Fri, 6 Jul 2007 14:00:59 +0000
Subject: 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
---
 doc/refman/RefMan-tac.tex | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'doc')

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
-- 
cgit v1.2.3