From 1a305fc0410e70fc36f59623d1f0e618f7ee9aab Mon Sep 17 00:00:00 2001
From: aspiwack
Date: Tue, 7 Feb 2012 16:51:57 +0000
Subject: Documentation for Grab Existential Variables.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14974 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 CHANGES                   | 2 ++
 doc/refman/RefMan-pro.tex | 7 +++++++
 2 files changed, 9 insertions(+)

diff --git a/CHANGES b/CHANGES
index 1fd72f7b08..b587e2ecc9 100644
--- a/CHANGES
+++ b/CHANGES
@@ -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 e5dc669dd5..4fa845310c 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}
-- 
cgit v1.2.3