diff options
| -rw-r--r-- | doc/refman/RefMan-tac.tex | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index b79d28138..bee91c952 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -1341,6 +1341,11 @@ existential variable from right to left in the conclusion. This cannot be the number of the existential variable since this number is different in every session. +When you are refering to hypotheses which you did not name +explicitely, be aware that Coq may make a different decision on how to +name the variable in the current goal and in the context of the +existential variable. This can lead to surprising behaviours. + \begin{Variants} \item {\tt instantiate ( {\num} := {\term} ) in \ident} |