Relecture v8

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

1 files changed, 14 insertions, 6 deletions

diff --git a/doc/RefMan-pro.tex b/doc/RefMan-pro.tex
index 79e0c82633..e8bcb3d7fa 100755
--- a/doc/RefMan-pro.tex
+++ b/doc/RefMan-pro.tex
@@ -52,8 +52,8 @@ that goal.
     Prop or Type}
 %\item \errindex{Proof objects can only be abstracted}
 %\item \errindex{A goal should be a type}
-\item \errindex{repeated goal not permitted in refining mode}
-the command {\tt Goal} cannot be used while a proof is already being edited.
+%\item \errindex{repeated goal not permitted in refining mode}
+%the command {\tt Goal} cannot be used while a proof is already being edited.
 \end{ErrMsgs}
 
 \SeeAlso section \ref{Theorem}
@@ -67,9 +67,9 @@ name is added to the environment as an {\tt Opaque} constant.
 
 \begin{ErrMsgs}
 \item \errindex{Attempt to save an incomplete proof}
-\item \ident\ \errindex{already exists}\\ 
-  The implicit name is already defined. You have then to provide
-  explicitly a new name (see variant 2 below).
+%\item \ident\ \errindex{already exists}\\ 
+%  The implicit name is already defined. You have then to provide
+%  explicitly a new name (see variant 3 below).
 \item Sometimes an error occurs when building the proof term,
 because tactics do not enforce completely the term construction
 constraints.
@@ -105,7 +105,15 @@ This command switches to interactive editing proof mode and declares
 as a {\tt Theorem}, the name {\ident} is known at all section levels:
 {\tt Theorem} is a {\sl global} lemma.
 
-\ErrMsg (see section \ref{Goal})
+%\ErrMsg (see section \ref{Goal})
+\begin{ErrMsgs}
+\item \errindex{the term \form\ has type \ldots{} which should be Set,
+    Prop or Type}
+\item \ident\ \errindex{already exists}\\ 
+  The name you provided already defined. You have then to choose
+  another name.
+\end{ErrMsgs}
+
 
 \begin{Variants}
 \item {\tt Lemma {\ident} : {\form}.}\comindex{Lemma}\\