Commit 8ad23fe1 authored by MARCHE Claude's avatar MARCHE Claude

doc: removed a few obsolete parts

parent 5f9b2016
......@@ -55,14 +55,14 @@ liblablgtk2-ocaml-dev liblablgtksourceview2-ocaml-dev
It is also installable from sources, available from the site
\url{http://wwwfun.kurims.kyoto-u.ac.jp/soft/olabl/lablgtk.html}
\item \todo{remove, obsolete} For \texttt{why3 bench}, the OCaml bindings of the sqlite3 library
are needed.
For Debian-based Linux distributions, you can install the package
\begin{verbatim}
libsqlite3-ocaml-dev
\end{verbatim}
It is also installable from sources, available from the site
\url{http://ocaml.info/home/ocaml_sources.html#ocaml-sqlite3}
% \item For \texttt{why3 bench}, the OCaml bindings of the sqlite3 library
% are needed.
% For Debian-based Linux distributions, you can install the package
% \begin{verbatim}
% libsqlite3-ocaml-dev
% \end{verbatim}
% It is also installable from sources, available from the site
% \url{http://ocaml.info/home/ocaml_sources.html#ocaml-sqlite3}
\end{itemize}
......
%\newcommand{\todo}[1]{{\Huge\bfseries TODO: #1}}
\newcommand{\why}{\textsf{Why3}\xspace}
\newcommand{\whyml}{\textsf{WhyML}\xspace}
\newcommand{\eg}{\emph{e.g.}\xspace}
......
......@@ -658,8 +658,6 @@ The available subcommands are as follows:
\item[\texttt{html}] outputs session contents in HTML format.
\item[\texttt{mod}] modifies some of the proofs, selected by a filter.
\item[\texttt{copy}] duplicates some of the proofs, selected by a filter.
\item[\texttt{copy-archive}] \todo{obsolete} same as copy but also archives the
original proofs\index{archived!proof attempt}.
\item[\texttt{rm}] removes some of the proofs, selected by a filter.
\end{description}
......@@ -711,7 +709,7 @@ the one hand if the proof suffers from an internal failure we mark it
with an exclamation mark \verb|!|, otherwise if it is not valid we
mark it with a question mark \verb|?|, finally if it is valid we add
nothing. On the other hand if the proof is obsolete we mark it with an
\verb|O| and if it is \todo{obsolete} archived we mark it with an \verb|A|.
\verb|O|.
For example, here are the session tree produced on the ``hello
proof'' example of Section~\ref{chap:starting}.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment