From cdbbcb3ebb9bed4bba558e6fa4a3b01f3cc18af1 Mon Sep 17 00:00:00 2001
From: glondu
Date: Thu, 23 Dec 2010 18:50:27 +0000
Subject: More precise documentation for instantiate

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

diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 6f1f8a13c4..977f68352d 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -950,7 +950,8 @@ existential variable.
 \tacindex{instantiate}
 \label{instantiate}}
 
-The {\tt instantiate} tactic allows to solve an existential variable
+The {\tt instantiate} tactic allows to refine (see Section~\ref{refine})
+an existential variable
 with the term \term. The \num\  argument is the position of the
 existential variable from right to left in the conclusion. This cannot be
 the number of the existential variable since this number is different
-- 
cgit v1.2.3