From b8d63929abec0e20b1ea971529650fb8cd54ee2f Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 2 Jun 2013 21:31:37 +0000
Subject: 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
---
 doc/refman/RefMan-tac.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'doc')

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}
-- 
cgit v1.2.3