Correction bug #1439 (comportement de replace by)

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

1 files changed, 4 insertions, 4 deletions

diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index d7d51ab23..d2753371b 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -533,8 +533,8 @@ in the list of subgoals remaining to prove.
 
 \item \texttt{assert {\form} by {\tac}}\tacindex{assert by}
   
-  This tactic behaves like \texttt{assert} but tries to apply {\tac}
-  to any subgoals generated by \texttt{assert}.
+  This tactic behaves like \texttt{assert} but applies {\tac}
+  to solve the subgoals generated by \texttt{assert}.
 
 \item \texttt{assert {\form} as {\ident}\tacindex{assert as}}
 
@@ -1708,8 +1708,8 @@ n}| assumption || symmetry; try assumption]}.
 
 \begin{Variants}
 \item {\tt replace {\term$_1$} with {\term$_2$} by \tac}\\ This acts
-  as {\tt replace {\term$_1$} with {\term$_2$}} but try to solve the
-  generated subgoal {\tt \term$_2$=\term$_1$} using {\tt \tac}.
+  as {\tt replace {\term$_1$} with {\term$_2$}} but applies {\tt \tac}
+  to solve the generated subgoal {\tt \term$_2$=\term$_1$}.
 \item {\tt replace {\term}}\\ Replace {\term} with {\term'} using the
   first assumption which type has the form {\tt \term=\term'} or {\tt
     \term'=\term}