From 208a0f7bfa5249f9795e6e225f309cbe715c0fad Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Tue, 21 Nov 2006 21:38:49 +0000 Subject: Imported Upstream version 8.1~gamma --- doc/refman/RefMan-ltac.tex | 15 +++++++++------ 1 file changed, 9 insertions(+), 6 deletions(-) (limited to 'doc/refman/RefMan-ltac.tex') 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} -- cgit v1.2.3