From 5519abf1bf1272eca36b63de69a7696f18342653 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond <guillaume.melquiond@inria.fr>
Date: Mon, 25 Jun 2018 07:57:45 +0200
Subject: [PATCH] Uniformize Sec. vs Section.
---
doc/install.tex | 6 +++---
doc/syntaxref.tex | 2 +-
doc/whyml.tex | 2 +-
3 files changed, 5 insertions(+), 5 deletions(-)
diff --git a/doc/install.tex b/doc/install.tex
index e74312345..8c61a5fb6 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 a861a5523..7577d4aca 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 4da89e5af..38c3b8ee7 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
--
GitLab