From 8a5f877b257133d12045e11ada64674e5a481ae6 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 24 Oct 2008 18:27:48 +0000
Subject: Fix doc of apply in (see coq-club message 26 September 2008)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11499 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 doc/refman/RefMan-tac.tex | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 00e8a3ecef..01ea532e66 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -473,7 +473,7 @@ Section~\ref{pattern} to transform the goal so that it gets the form
   {\bindinglist$_1$}} {\tt ,} \ldots {\tt ,} {\term$_n$} \zeroone{{\tt with}
   {\bindinglist$_n$}}
 
-  This summarizes the difference syntaxes for {\tt apply}.
+  This summarizes the different syntaxes for {\tt apply}.
 
 \item {\tt lapply {\term}} \tacindex{lapply} 
 
@@ -647,7 +647,7 @@ hypothesis of the context.  The tactic {\tt apply {\term} in {\ident}}
 tries to match the conclusion of the type of {\ident} against a non
 dependent premises of the type of {\term}, trying them from right to
 left.  If it succeeds, the statement of hypothesis {\ident} is
-replaced by the conclusion of the type of {\ident}. The tactic also
+replaced by the conclusion of the type of {\term}. The tactic also
 returns as many subgoals as the number of other non dependent premises
 in the type of {\term} and of the non dependent premises of the type
 of {\ident}.  The tactic {\tt apply} relies on first-order
-- 
cgit v1.2.3