From 6d958b5ddc2cc621d3bf8ca005de587c82b88cbf Mon Sep 17 00:00:00 2001
From: marche
Date: Fri, 12 Dec 2003 15:04:08 +0000
Subject: subtree no

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8388 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 doc/RefMan-pro.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/doc/RefMan-pro.tex b/doc/RefMan-pro.tex
index a65cd816e4..79e0c82633 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
-- 
cgit v1.2.3