3 files changed, 56 insertions, 8 deletions
diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex
index e7400232c..ad2ffdc63 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}
diff --git a/doc/refman/RefMan-pre.tex b/doc/refman/RefMan-pre.tex
index 6aaca9668..cac79625a 100644
--- a/doc/refman/RefMan-pre.tex
+++ b/doc/refman/RefMan-pre.tex
@@ -539,6 +539,9 @@ Benjamin Grégoire, Assia Mahboubi and Bruno Barras developed a new
 more efficient and more general simplification algorithm on rings and
 semi-rings.
 
+Laurent Théry and Bruno Barras developed a new significantly more efficient
+simplification algorithm on fields.
+
 Hugo Herbelin, Pierre Letouzey, Julien Forest, Julien Narboux and
 Claudio Sacerdoti Coen added new tactic features.
 
@@ -567,8 +570,8 @@ Pierre Corbineau extended his tactic for solving first-order
 statements. He wrote a reflection-based intuitionistic tautology
 solver.
 
-Pierre Courtieu and Julien Forest added extra support to reason on the
-inductive structure of recursively defined functions.
+Pierre Courtieu, Julien Forest and Yves Bertot added extra support to
+reason on the inductive structure of recursively defined functions.
 
 Jean-Marc Notin significantly contributed to the general maintenance
 of the system. He also took care of {\textsf{coqdoc}}.
@@ -576,6 +579,9 @@ of the system. He also took care of {\textsf{coqdoc}}.
 Pierre Castéran contributed to the documentation of (co-)inductive
 types and suggested improvements to the libraries.
 
+Pierre Corbineau implemented a declarative mathematical proof
+language, usable in combination with the tactic-based style of proof.
+
 Finally, many users suggested improvements of the system through the
 Coq-Club mailing list and bug-tracker systems, especially user groups
 from INRIA Rocquencourt, Radbout University, University of
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 315286571..a29dcbfd8 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -577,6 +577,45 @@ in the list of subgoals remaining to prove.
 %  \term\ will be kept.
 %\end{Variants}
 
+\subsection{{\tt apply {\term} in {\ident}}
+\tacindex{apply {\ldots} in}}
+
+This tactic applies to any goal.  The argument {\term} is a term
+well-formed in the local context and the argument {\ident} is an
+hypothesis of the context.  The tactic {\tt apply {\term} in {\ident}}
+tries to match the conclusion of the type of {\ident} against a non
+dependent premisses of the type of {\term}, trying them from right to
+left.  If it succeeds, the statement of hypothesis {\ident} is
+replaced by the conclusion of the type of {\ident}. The tactic also
+returns as many subgoals as the number of other non dependent premises
+in the type of {\term} and of the non dependent premises of the type
+of {\ident}.  The tactic {\tt apply} relies on first-order
+pattern-matching with dependent types.
+
+\begin{ErrMsgs}
+\item \errindex{Statement without assumptions}
+
+This happens if the type of {\term} has no non dependent premise.
+
+\item \errindex{Unable to apply}
+
+This happens if the conclusion of {\ident} does not match any of the
+non dependent premises of the type of {\term}.
+\end{ErrMsgs}
+
+\begin{Variants}
+\item {\tt apply \nelist{\term}{,} in {\ident}}
+
+This applies each of {\term} in sequence in {\ident}.
+
+\item {\tt apply \nelist{{\term} {\bindinglist}}{,} in {\ident}}
+
+This does the same but uses the bindings in each {\bindinglist} to 
+instanciate the parameters of the corresponding type of {\term}
+(see syntax of bindings in Section~\ref{Binding-list}).
+
+\end{Variants}
+
 \subsection{\tt generalize \term
 \tacindex{generalize}
 \label{generalize}}