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 | |
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
-rw-r--r-- | CHANGES | 2 | ||||
-rw-r--r-- | doc/refman/RefMan-pro.tex | 7 |
2 files changed, 9 insertions, 0 deletions
@@ -12,6 +12,8 @@ Vernacular commands - New command "Set Parsing Explicit" for deactivating parsing (and printing) of implicit arguments (useful for teaching). +- New command "Grab Existential Variables" to transform the unresolved evars at + the end of a proof into goals. Tactics 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} |