diff options
| author |  aspiwack <aspiwack@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-02-07 16:51:57 +0000 |
|---|---|---|
| committer | aspiwack <aspiwack@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-02-07 16:51:57 +0000 |
| commit | 1a305fc0410e70fc36f59623d1f0e618f7ee9aab (patch) | |
| tree | 0612b27ca05b00d84a84e2f492c83b320f517786 /doc/refman | |
| parent | 8e30bdf78eb5feb274b16fb1db1c7350e771ee99 (diff) | |
Documentation for Grab Existential Variables.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14974 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'doc/refman')
| -rw-r--r-- | doc/refman/RefMan-pro.tex | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex index e5dc669dd..4fa845310 100644 --- a/doc/refman/RefMan-pro.tex +++ b/doc/refman/RefMan-pro.tex @@ -216,7 +216,14 @@ existential variables remain. To instantiate existential variables during proof edition, you should use the tactic {\tt instantiate}. \SeeAlso {\tt instantiate (\num:= \term).} in Section~\ref{instantiate}. +\SeeAlso {\tt Grab Existential Variables.} below. +\subsection[\tt Grab Existential Variables.]{\tt Grab Existential Variables.\comindex{Grab Existential Variables} +\label{GrabEvars}} + +This command can be run when a proof has no more goal to be solved but has remaining +uninstantiated existential variables. It takes every uninstantiated existential variable +and turns it into a goal. %%%%%%%% \section{Navigation in the proof tree} |