diff options
| -rw-r--r-- | doc/refman/RefMan-tac.tex | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index a02b0a5e53..432ff52796 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -2007,7 +2007,7 @@ the given bindings to instantiate parameters or hypotheses of {\term}. This behaves like {\tt discriminate {\ident}} if {\ident} is the name of an hypothesis to which {\tt discriminate} is applicable; if the current goal is of the form {\term$_1$} {\tt <>} {\term$_2$}, - this behaves as {\tt intro {\ident}; injection {\ident}}. + this behaves as {\tt intro {\ident}; discriminate {\ident}}. \ErrMsg \errindex{No discriminable equalities} \end{Variants} |