From 74c29c96afef4b30778fa892eeecfb6c743d8add Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond <guillaume.melquiond@inria.fr> Date: Sat, 23 Jun 2018 09:00:25 +0200 Subject: [PATCH] Fix broken links. --- doc/api.tex | 4 ++-- doc/exec.tex | 10 ++++++++-- doc/whyml.tex | 1 + 3 files changed, 11 insertions(+), 4 deletions(-) diff --git a/doc/api.tex b/doc/api.tex index a2e18db72..4a023f03b 100644 --- a/doc/api.tex +++ b/doc/api.tex @@ -189,8 +189,8 @@ constructed. Here is the way we build the formula $2+2=4$. The main difficulty is to access the internal identifier for addition: it must be retrieved from -the standard theory \texttt{Int} of the file \texttt{int.why} (see -Chap~\ref{sec:library}). +the standard theory \texttt{Int} of the file \texttt{int.why}. +% (see Chap~\ref{sec:library}). \lstinputlisting{generated/logic__buildfmla.ml} An important point to notice as that when building the application of $+$ to the arguments, it is checked that the types are correct. Indeed diff --git a/doc/exec.tex b/doc/exec.tex index dc44f40a7..231e47fa5 100644 --- a/doc/exec.tex +++ b/doc/exec.tex @@ -118,8 +118,14 @@ extraction command line: \paragraph{Examples.} We illustrate different ways of using the \texttt{extract} command through some -examples. Consider the program in Figure~\ref{fig:AQueue} on -page~\pageref{fig:AQueue}. If we are only interested in extracting function +examples. +\begin{latexonly} +Consider the program in Figure~\ref{fig:AQueue} on page~\pageref{fig:AQueue}. +\end{latexonly} +\begin{htmlonly} +Consider the program of Section~\ref{sec:AQueue}. +\end{htmlonly} +If we are only interested in extracting function \texttt{enqueue}, we can proceed as follows: \begin{verbatim} > why3 extract -D ocaml64 -L . aqueue.AmortizedQueue.enqueue -o aqueue.ml diff --git a/doc/whyml.tex b/doc/whyml.tex index 89ab4837b..5683455cb 100644 --- a/doc/whyml.tex +++ b/doc/whyml.tex @@ -931,6 +931,7 @@ end %END LATEX \section{Problem 5: Amortized Queue} +\label{sec:AQueue} The last problem consists in verifying the implementation of a well-known purely applicative data structure for queues. -- GitLab