Commit 5ffd6fc3 authored by MARCHE Claude's avatar MARCHE Claude

doc de why3doc, roadmap updated

parent 93d18c1c
......@@ -148,7 +148,7 @@ dans l'IDE
** DONE option timelimit <n>
** DONE renommer "coq-plugin" en "coq-tactic"
* (JCF, ANDREI) add all examples from the VSTTE 2012 competition
* DONE (JCF, ANDREI) add all examples from the VSTTE 2012 competition
* DONE (CLAUDE) Ajouter page provers sur le site web why3
** !TODO! relire
......
......@@ -12,9 +12,10 @@ provided by the \why environment. These are as follows:
\item[\texttt{why3ml}] as \texttt{why3} but reads \why{} ML programs instead
\item[\texttt{why3replayer}] replay the proofs stored in a session,
for regression test purposes
\item[\texttt{why3bench}] produces benchmarks
\item[\texttt{why3bench}] produces benchmarks \todo{obsolete ?}
\item[\texttt{why3session}] dumps various informations from a proof
session, and possibly modifies the session.
\item[\texttt{why3doc}] produces HTML versions of \why source codes.
\end{description}
All these tools accept a common subset of command-line options. In
......@@ -793,6 +794,14 @@ proof is not replayed by why3replayer.
\section{The \texttt{why3doc} tool}
\label{sec:why3doc}
\todo{Documenter}
%%% Local Variables:
%%% mode: latex
%%% TeX-PDF-mode: t
......
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