diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/refman/RefMan-tac.tex | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index fa0e04534..9bba45bea 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -1341,10 +1341,10 @@ 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 +When you are referring 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. +existential variable. This can lead to surprising behaviors. \begin{Variants} \item {\tt instantiate ( {\num} := {\term} ) in \ident} |