diff options
| -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} |