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
---
 doc/refman/RefMan-pro.tex | 7 +++++++
 1 file changed, 7 insertions(+)

(limited to 'doc')

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