Fixing a typo in the documentation of discriminate.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16551 85f007b7-540e-0410-9357-904b9bb8a0f7

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}