Documentation de "instantiate".

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11080 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 9 insertions, 0 deletions

diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index ffee048d1..7bdc35cf8 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