From 208a0f7bfa5249f9795e6e225f309cbe715c0fad Mon Sep 17 00:00:00 2001
From: Samuel Mimram <smimram@debian.org>
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

