diff options
| author |  glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-12-23 18:50:27 +0000 |
|---|---|---|
| committer | glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-12-23 18:50:27 +0000 |
| commit | cdbbcb3ebb9bed4bba558e6fa4a3b01f3cc18af1 (patch) | |
| tree | a2c428d8a295c790737e7ec37c060956d56f65f3 | |
| parent | e3696e15775c44990018d1d4aea01c9bf662cd73 (diff) | |
More precise documentation for instantiate
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13741 85f007b7-540e-0410-9357-904b9bb8a0f7
| -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 6f1f8a13c..977f68352 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 |