diff options
author | 2017-06-12 12:16:34 +0200 | |
---|---|---|
committer | 2017-06-13 09:42:38 +0200 | |
commit | 5cc502fe1b60f59815dfa2819e169dc7ae9b4c7e (patch) | |
tree | bbe238b2b76f425d0f7dd513b7884829d45bfbcd /doc/refman | |
parent | 39f36789b986779d36acd36cfa1425487bad43c3 (diff) |
Document Show ident.
Diffstat (limited to 'doc/refman')
-rw-r--r-- | doc/refman/RefMan-pro.tex | 18 |
1 files changed, 18 insertions, 0 deletions
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. |