From a36f148dd86a258cd15f5a24678caa3ad7bb76ca Mon Sep 17 00:00:00 2001
From: glondu
Date: Mon, 9 Jun 2008 15:11:59 +0000
Subject: Documentation de "instantiate".

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11080 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 doc/refman/RefMan-tac.tex | 9 +++++++++
 1 file changed, 9 insertions(+)

(limited to 'doc')

diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index ffee048d12..7bdc35cf8e 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -833,6 +833,15 @@ in every session.
 These allow to refer respectively to existential variables occurring in 
 a hypothesis or in the body or the type of a local definition.  
 
+  \item {\tt instantiate}
+
+    Without argument, the {\tt instantiate} tactic tries to solve as
+    many existential variables as possible, using information gathered
+    from other tactics in the same tactical. This is automatically
+    done after each complete tactic (i.e. after a dot in proof mode),
+    but not, for example, between each tactic when they are sequenced
+    by semicolons.
+
 \end{Variants}
 
 \subsection{Bindings list
-- 
cgit v1.2.3