From 14787df2ea09994151e886bf918aca0aecbd8ade Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 24 Jan 2015 20:08:53 +0100
Subject: Reference Manual: Documenting new printing of evars and new effect of
 Set Printing Existential Instances (see bug report #3951).

---
 doc/refman/RefMan-tac.tex | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

(limited to 'doc/refman/RefMan-tac.tex')

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}
-- 
cgit v1.2.3