diff --git a/doc/api.tex b/doc/api.tex index a2e18db728f1aa7b4d51ab09315d5992f4dd7a46..4a023f03b6bc32d3dd737519db72d63458393a28 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 dc44f40a78cbfd7d327d00248f1fc60316cecd09..231e47fa5e390566363e7bfafb76d7e7eb2563be 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 89ab4837b9bec671a1a2565e318ef2e09eef4694..5683455cbfd0f15fca3c3937666c25aa75e17d16 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.