Document evar naming syntax.

2 files changed, 6 insertions, 1 deletions

diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex
index b475a5233..3f2dd73a3 100644
--- a/doc/refman/RefMan-ext.tex
+++ b/doc/refman/RefMan-ext.tex
@@ -1990,6 +1990,11 @@ Check (fun x y => _) 0 1.
 Unset Printing Existential Instances.
 \end{coq_eval}
 
+Existential variables can be named by the user upon creation using
+the syntax {\tt ?[\ident]}. This is useful when the existential
+variable needs to be explicitly handled later in the script (e.g.
+with a named-goal selector, see~\ref{ltac:selector}).
+
 \subsection{Explicit displaying of existential instances for pretty-printing
 \label{SetPrintingExistentialInstances}
 \optindex{Printing Existential Instances}}
diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex
index 9378529cb..9caea8f39 100644
--- a/doc/refman/RefMan-ltac.tex
+++ b/doc/refman/RefMan-ltac.tex
@@ -392,7 +392,7 @@ all selected goals.
   \item{} [{\ident}] {\tt :} {\tacexpr}
 
     In this variant, {\tacexpr} is applied locally to a goal
-    previously named by the user.
+    previously named by the user (see~\ref{ExistentialVariables}).
 
   \item {\num} {\tt :} {\tacexpr}