From 5cc502fe1b60f59815dfa2819e169dc7ae9b4c7e Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Mon, 12 Jun 2017 12:16:34 +0200
Subject: Document Show ident.

---
 doc/refman/RefMan-pro.tex | 18 ++++++++++++++++++
 1 file changed, 18 insertions(+)

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

diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex
index 4c333379bd..9c211b00f3 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. 
-- 
cgit v1.2.3

