From d3ac30ae99a9e56bdf0718487a4607e1fae79242 Mon Sep 17 00:00:00 2001 From: notin Date: Tue, 13 Mar 2007 14:45:21 +0000 Subject: 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 --- doc/refman/RefMan-tac.tex | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'doc/refman/RefMan-tac.tex') 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} -- cgit v1.2.3