diff --git a/Version b/Version index a39c99a07b38f04db939aa82886f048da924278b..9f991a32dd15568dbc7a786f0201fd99680d07ce 100644 --- a/Version +++ b/Version @@ -1,5 +1,5 @@ # Why version -VERSION=0.81 +VERSION=0.81+git diff --git a/doc/api.tex b/doc/api.tex index fe7b9f79ad68a643c0f13cdf5c5ff5e6fcbdc5bc..de5f5409e610b6c2fbe8062b0fd676e464891272 100644 --- a/doc/api.tex +++ b/doc/api.tex @@ -6,19 +6,21 @@ OCaml code with the \why library. We progressively introduce the way one can use the library to build terms, formulas, theories, proof tasks, call external provers on tasks, and apply transformations on tasks. The complete documentation for API calls is given -at URL~\url{http://why3.lri.fr/api/}. +at URL~\url{http://why3.lri.fr/api-\whyversion/}. We assume the reader has a fair knowledge of the OCaml language. Notice that the \why library must be installed, see Section~\ref{sec:installlib}. The OCaml code given below is available in -the source distribution as \verb|examples/use_api/use_api.ml|. +the source distribution in directory \verb|examples/use_api/| together +with a few other examples. \section{Building Propositional Formulas} The first step is to know how to build propositional formulas. The module \texttt{Term} gives a few functions for building these. Here is -a piece of OCaml code for building the formula $\mathit{true} \lor \mathit{false}$. +a piece of OCaml code for building the formula $\mathit{true} \lor +\mathit{false}$. \begin{ocamlcode} (* opening the Why3 library *) open Why3