diff options
author | Samuel Mimram <smimram@debian.org> | 2006-11-21 21:38:49 +0000 |
---|---|---|
committer | Samuel Mimram <smimram@debian.org> | 2006-11-21 21:38:49 +0000 |
commit | 70b9be8acc1d1ada178a95c1cd4013506e9d0d1b (patch) | |
tree | f672a286d962cc67c95874b3b60402fc957870b6 /doc/refman/RefMan-ltac.tex | |
parent | a5bd4e097a94cc4f863bf4d4bcc5ce592c30ba47 (diff) | |
parent | 208a0f7bfa5249f9795e6e225f309cbe715c0fad (diff) |
Merge commit 'upstream/8.1.gamma' into 8.1
Diffstat (limited to 'doc/refman/RefMan-ltac.tex')
-rw-r--r-- | doc/refman/RefMan-ltac.tex | 15 |
1 files changed, 9 insertions, 6 deletions
diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex index e7400232..ad2ffdc6 100644 --- a/doc/refman/RefMan-ltac.tex +++ b/doc/refman/RefMan-ltac.tex @@ -660,14 +660,17 @@ replaces the hole of the value of {\ident} by the value of Tactics sometimes have to generate new names for hypothesis. Letting the system decide a name with the {\tt intro} tactic is not so good since it is very awkward to retrieve the name the system gave. - -As before, the following expression returns a term: +The following expression returns an identifier: \begin{quote} -{\tt fresh} {\qstring} +{\tt fresh} \nelist{\textrm{\textsl{component}}}{} \end{quote} -It evaluates to an identifier unbound in the goal, which is obtained -by padding {\qstring} with a number if necessary. If no name is given, -the prefix is {\tt H}. +It evaluates to an identifier unbound in the goal. This fresh +identifier is obtained by concatenating the value of the +\textrm{\textsl{component}}'s (each of them is, either an {\ident} which +has to refer to a name, or directly a name denoted by a +{\qstring}). If the resulting name is already used, it is padded +with a number so that it becomes fresh. If no component is +given, the name is a fresh derivative of the name {\tt H}. \subsubsection{Computing in a constr} \index{Ltac!eval} |