1 files changed, 9 insertions, 9 deletions

diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex
index 1a004b6657..d0ca097473 100644
--- a/doc/refman/RefMan-pro.tex
+++ b/doc/refman/RefMan-pro.tex
@@ -2,12 +2,12 @@
 \label{Proof-handling}}
 
 In \Coq's proof editing mode all top-level commands documented in 
-chapter \ref{Vernacular-commands} remain available
+Chapter~\ref{Vernacular-commands} remain available
 and the user has access to specialized commands dealing with proof
 development pragmas documented in this section. He can also use some
 other specialized commands called {\em tactics}.  They are the very
 tools allowing the user to deal with logical reasoning. They are
-documented in chapter \ref{Tactics}.\\ 
+documented in Chapter~\ref{Tactics}.\\ 
 When switching in editing proof mode, the prompt
 \index{Prompt} 
 {\tt Coq <} is changed into {\tt {\ident} <} where {\ident} is the
@@ -21,7 +21,7 @@ generated by the tactics.
 To each subgoal is associated  a number of
 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}).
+certain tactics (see mainly Section~\ref{intro}).
 
 When a proof is achieved the message {\tt Proof completed} is
 displayed. One can then store this proof as a defined constant in the
@@ -54,7 +54,7 @@ that goal.
 %the command {\tt Goal} cannot be used while a proof is already being edited.
 \end{ErrMsgs}
 
-\SeeAlso section \ref{Theorem}
+\SeeAlso Section~\ref{Theorem}
 
 \subsection[\tt Qed.]{\tt Qed.\comindex{Qed}\label{Qed}}
 This command is available in interactive editing proof mode when the
@@ -117,7 +117,7 @@ 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}
 
@@ -164,7 +164,7 @@ as a {\tt Theorem}, the name {\ident} is known at all section levels:
 \label{BeginProof}}
 This command applies in proof editing mode. It is equivalent to {\tt
   exact {\term}; Save.} That is, you have to give the full proof in
-one gulp, as a proof term (see section \ref{exact}).
+one gulp, as a proof term (see Section~\ref{exact}).
 
 \variant {\tt Proof.}
   
@@ -173,7 +173,7 @@ one gulp, as a proof term (see section \ref{exact}).
   practice to use {\tt Proof.} as an opening parenthesis, closed in
   the script with a closing {\tt Qed.}
 
-\SeeAlso {\tt Proof with {\tac}.} in section~\ref{ProofWith}.
+\SeeAlso {\tt Proof with {\tac}.} in Section~\ref{ProofWith}.
 
 \subsection[\tt Abort.]{\tt Abort.\comindex{Abort}}
 
@@ -232,14 +232,14 @@ This commands switches back to the editing of the last edited proof.
 
 This command allows to instantiate an existential variable. {\tt \num}
 is an index in the list of uninstantiated existential variables
-displayed by {\tt Show Existentials.} (described in section~\ref{Show})
+displayed by {\tt Show Existentials.} (described in Section~\ref{Show})
 
 This command is intented to be used to instantiate existential
 variables when the proof is completed but some uninstantiated
 existential variables remain. To instantiate existential variables
 during proof edition, you should use the tactic {\tt instantiate}.
 
-\SeeAlso {\tt instantiate (\num:= \term).} in section~\ref{instantiate}.
+\SeeAlso {\tt instantiate (\num:= \term).} in Section~\ref{instantiate}.
 
 
 %%%%%%%%