diff --git a/doc/install.tex b/doc/install.tex
index e743123457d7eacc1b7c40ccd995637b6e927f05..8c61a5fb6e01d3f0792b9fcb4b8a83a679841374 100644
--- a/doc/install.tex
+++ b/doc/install.tex
@@ -12,7 +12,7 @@ package manager. It is as simple as
 \begin{verbatim}
 > opam install why3
 \end{verbatim}
-Then jump to Sec.~\ref{provers} to install external provers.
+Then jump to Section~\ref{provers} to install external provers.
 
 \subsection{Installation Instructions from Source Distribution}
 
@@ -85,7 +85,7 @@ make install
 \end{verbatim}
 Installation can be tested as follows:
 \begin{enumerate}
-\item install some external provers (see~Sec.~\ref{provers} below)
+\item install some external provers (see Section~\ref{provers} below)
 \item run \verb|why3 config --detect|
 \item run some examples from the distribution, \eg you should
 obtain the following (provided the required provers are installed on
@@ -137,7 +137,7 @@ have to run the following command:
 > why3 config --detect
 \end{verbatim}
 It scans your \texttt{PATH} for provers and updates your configuration
-file (see Sec.~\ref{sec:why3config}) accordingly.
+file (see Section~\ref{sec:why3config}) accordingly.
 
 \subsection{Multiple Versions of the Same Prover}
 
diff --git a/doc/syntaxref.tex b/doc/syntaxref.tex
index a861a55233fc11ca99c6e97288fad847aea5db26..7577d4aca9914b0d3c397ebbbeb48b715b537f09 100644
--- a/doc/syntaxref.tex
+++ b/doc/syntaxref.tex
@@ -733,7 +733,7 @@ indexed by 63-bit integers are imported as follows:
 \end{whycode}
 In particular, the types and operations from these modules are mapped
 to native OCaml's types and operations when \why code is extracted to
-OCaml (see Sec.~\ref{sec:extract}).
+OCaml (see Section~\ref{sec:extract}).
 
 %%% Local Variables:
 %%% mode: latex
diff --git a/doc/whyml.tex b/doc/whyml.tex
index 4da89e5afee572b44b82f9b3ab67b3fe0f2c3208..38c3b8ee770bdb193ea4e6602f9388df3dadbb95 100644
--- a/doc/whyml.tex
+++ b/doc/whyml.tex
@@ -56,7 +56,7 @@ See Chapter~\ref{chap:manpages} for more details regarding command lines.
 
 \medskip
 As an introduction to \whyml, we use a small logical puzzle
-(Sec.~\ref{sec:Einstein}) and then the five problems from the VSTTE
+(Section~\ref{sec:Einstein}) and then the five problems from the VSTTE
 2010 verification competition~\cite{vstte10comp}.
 The source code for all these examples is contained in \why's
 distribution, in sub-directory \texttt{examples/}. Look for files