Reference Manual: Documenting new printing of evars and new effect of

Set Printing Existential Instances (see bug report #3951).

1 files changed, 5 insertions, 5 deletions

diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 1b7adc2517..35da17d546 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -260,6 +260,7 @@ Defined.
 \subsection{\tt apply \term}
 \tacindex{apply}
 \label{apply}
+\label{eapply}
 
 This tactic applies to any goal.  The argument {\term} is a term
 well-formed in the local context.  The tactic {\tt apply} tries to
@@ -329,14 +330,13 @@ Section~\ref{pattern} to transform the goal so that it gets the form
    generated by {\tt apply} {\term$_i$}, starting from the application
    of {\term$_1$}.
 
-\item {\tt eapply \term}\tacindex{eapply}\label{eapply}
+\item {\tt eapply \term}\tacindex{eapply}
 
   The tactic {\tt eapply} behaves like {\tt apply} but it does not fail
   when no instantiations are deducible for some variables in the
-  premises.  Rather, it turns these variables into so-called
-  existential variables which are variables still to instantiate. An
-  existential variable is identified by a name of the form {\tt ?$n$}
-  where $n$ is a number.  The instantiation is intended to be found
+  premises. Rather, it turns these variables into 
+  existential variables which are variables still to instantiate (see
+  Section~\ref{evars}). The instantiation is intended to be found
   later in the proof.
 
 \item {\tt simple apply {\term}} \tacindex{simple apply}