Merge PR#767: Document named evars (including Show ident)

4 files changed, 41 insertions, 8 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}
 
diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex
index 4c333379b..9c211b00f 100644
--- a/doc/refman/RefMan-pro.tex
+++ b/doc/refman/RefMan-pro.tex
@@ -434,6 +434,24 @@ This command displays the current goals.
 \item \errindex{No focused proof}
 \end{ErrMsgs}
 
+\item {\tt Show {\ident}.}\\
+  Displays the named goal {\ident}.
+  This is useful in particular to display a shelved goal but only works
+  if the corresponding existential variable has been named by the user
+  (see~\ref{ExistentialVariables}) as in the following example.
+
+\begin{coq_eval}
+Reset Initial.
+\end{coq_eval}
+
+\begin{coq_example*}
+Goal exists n, n = 0.
+  eexists ?[n].
+\end{coq_example*}
+\begin{coq_example}
+  Show n.
+\end{coq_example}
+
 \item {\tt Show Script.}\comindex{Show Script}\\
   Displays the whole list of tactics applied from the beginning
   of the current proof. 
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 3f1241186..9707a6c72 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -1429,23 +1429,33 @@ The {\tt evar} tactic creates a new local definition named \ident\ with
 type \term\ in the context. The body of this binding is a fresh
 existential variable.
 
-\subsection{\tt instantiate ( {\num} := {\term} )}
+\subsection{\tt instantiate ( {\ident} := {\term} )}
 \tacindex{instantiate}
 \label{instantiate}
 
 The {\tt instantiate} tactic refines (see Section~\ref{refine})
-an existential variable
-with the term \term. The \num\  argument is the position of the
-existential variable from right to left in the conclusion. This cannot be
-the number of the existential variable since this number is different
-in every session.
+an existential variable {\ident} with the term {\term}.
+It is equivalent to {\tt only [\ident]: refine \term} (preferred alternative).
 
-When you are referring to hypotheses which you did not name
+\begin{Remarks}
+\item To be able to refer to an existential variable by name, the
+user must have given the name explicitly (see~\ref{ExistentialVariables}).
+
+\item When you are referring to hypotheses which you did not name
 explicitly, be aware that Coq may make a different decision on how to
 name the variable in the current goal and in the context of the
 existential variable. This can lead to surprising behaviors.
+\end{Remarks}
 
 \begin{Variants}
+
+  \item {\tt instantiate ( {\num} := {\term} )}
+  This variant allows to refer to an existential variable which was not
+  named by the user. The {\num} argument is the position of the
+  existential variable from right to left in the goal.
+  Because this variant is not robust to slight changes in the goal,
+  its use is strongly discouraged.
+
   \item {\tt instantiate ( {\num} := {\term} ) in \ident}
 
   \item {\tt instantiate ( {\num} := {\term} ) in ( Value of {\ident} )}