diff options
| -rw-r--r-- | doc/refman/RefMan-tac.tex | 3 |
1 files changed, 2 insertions, 1 deletions
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 |