V7

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

1 files changed, 11 insertions, 0 deletions

diff --git a/doc/Tutorial.tex b/doc/Tutorial.tex
index f1d8123cbe..a525c5a213 100755
--- a/doc/Tutorial.tex
+++ b/doc/Tutorial.tex
@@ -976,9 +976,20 @@ symmetry of equality, for instance with tactics \verb:Transitivity: and
 \begin{coq_example}
 Apply foo.
 Transitivity (f O); Symmetry; Trivial.
+\end{coq_example}
+In case the equality $t=u$ generated by \verb:Replace: $u$ \verb:with:
+$t$ is an assumption
+(possibly modulo symmetry), it will be automatically proved and the
+corresponding goal will not appear. For instance:
+\begin{coq_example}
+Restart.
+Replace (f O) with O.
+Rewrite f10; Rewrite foo; Trivial.
 Save.
 \end{coq_example}
 
+
+
 \subsection{Predicate calculus over Type}
 
 We just explained the basis of first-order reasoning in the universe