subtree no

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

1 files changed, 1 insertions, 1 deletions

diff --git a/doc/RefMan-pro.tex b/doc/RefMan-pro.tex
index a65cd816e..79e0c8263 100755
--- a/doc/RefMan-pro.tex
+++ b/doc/RefMan-pro.tex
@@ -24,7 +24,7 @@ hypotheses we call the {\em \index*{local context}} of the goal.
 Initially, the local context is empty. It is enriched by the use of
 certain tactics (see mainly section \ref{Intro}).
 
-When a proof is achieved the message {\tt Subtree proved!} is
+When a proof is achieved the message {\tt Proof completed} is
 displayed. One can then store this proof as a defined constant in the
 environment. Because there exists a correspondence between proofs and
 terms of $\lambda$-calculus, known as the {\em Curry-Howard