diff --git a/doc/HelloProof-style2.tex b/doc/HelloProof-style2.tex
index 507330e7fbef198b388ab1be16b4907fc8bdbd11..c0f3b7471856f5c7aa988d498d71b684a521ac34 100644
--- a/doc/HelloProof-style2.tex
+++ b/doc/HelloProof-style2.tex
@@ -1,15 +1,15 @@
-\begin{tabular}{| l |c |c |c |c |c |}
-\hline Proof obligations & \provername{Alt-Ergo (0.94)} & \provername{Coq (8.3pl4)} & \provername{Simplify (1.5.4)} \\
-\hline
-\explanation{G1} & \noresult& \noresult& \valid{0.00} \\
-\hline
-\explanation{G2} & \unknown{0.00} & \noresult& \unknown{0.00} \\
-\cline{2-4}
-\quad\transformation{split\_goal} & \multicolumn{3}{|c|}{}\\
-\cline{2-4}
-\quad\subgoal{1.}{1} & \unknown{0.00} & \unknown{0.43} & \unknown{0.00} \\
-\cline{2-4}
-\quad\subgoal{2.}{2} & \valid{0.00} & \noresult& \valid{0.00} \\
-\hline
-\explanation{G3} & \valid{0.00} & \noresult& \unknown{0.00} \\
+\begin{tabular}{|l|l|l|l|c|c|}
+\hline Proof obligations & \provername{Alt-Ergo 0.99.1} & \provername{Coq 8.7.1} \\
+\hline
+\explanation{G1} & \valid{0.00} & \noresult\\
+\hline
+\explanation{G2} & \unknown{0.00} & \noresult\\
+\cline{2-3}
+\quad\transformation{split\_goal\_right} & \multicolumn{2}{|c|}{}\\
+\cline{2-3}
+\quad\subgoal{G2.0}{1} & \unknown{0.00} & \unknown{0.29} \\
+\cline{2-3}
+\quad\subgoal{G2.1}{2} & \valid{0.00} & \noresult\\
+\hline
+\explanation{G3} & \valid{0.00} & \noresult\\
\hline \end{tabular}
diff --git a/doc/HelloProof.tex b/doc/HelloProof.tex
index e587907348129aca8541f5126cf64804aa0e9914..0d32e4683b13b4b2e851557f8da911ec30b94101 100644
--- a/doc/HelloProof.tex
+++ b/doc/HelloProof.tex
@@ -1,13 +1,13 @@
-\begin{tabular}{| l |c |c |c |c |c |}
-\hline \multicolumn{2}{|c|}{Proof obligations } & \provername{Alt-Ergo (0.94)} & \provername{Coq (8.3pl4)} & \provername{Simplify (1.5.4)} \\
-\hline
-\explanation{G1} & & \noresult& \noresult& \valid{0.00} \\
-\hline
-\explanation{G2} & & \unknown{0.00} & \noresult& \unknown{0.00} \\
-\cline{2-4}
- & \explanation{1.} & \unknown{0.00} & \unknown{0.43} & \unknown{0.00} \\
-\cline{2-5}
- & \explanation{2.} & \valid{0.00} & \noresult& \valid{0.00} \\
-\hline
-\explanation{G3} & & \valid{0.00} & \noresult& \unknown{0.00} \\
+\begin{tabular}{|l|l|l|l|c|c|}
+\hline \multicolumn{2}{|c|}{Proof obligations } & \provername{Alt-Ergo 0.99.1} & \provername{Coq 8.7.1} \\
+\hline
+\explanation{G1} & & \valid{0.00} & \noresult\\
+\hline
+\explanation{G2} & & \unknown{0.00} & \noresult\\
+\cline{2-3}
+ & \explanation{G2.0} & \unknown{0.00} & \unknown{0.29} \\
+\cline{2-4}
+ & \explanation{G2.1} & \valid{0.00} & \noresult\\
+\hline
+\explanation{G3} & & \valid{0.00} & \noresult\\
\hline \end{tabular}
diff --git a/doc/hello_proof.png b/doc/hello_proof.png
index 922d6cf39851f32372373672141075cdcaa24cea..fc552d9c41eb938628adb8ec71ec201a1c6a7ac1 100644
Binary files a/doc/hello_proof.png and b/doc/hello_proof.png differ
diff --git a/doc/manpages.tex b/doc/manpages.tex
index dd89acde23a77e20830efb111716bffb9af8c60e..2e06c2a692d5e037926a9e623bc6ac602e60a58e 100644
--- a/doc/manpages.tex
+++ b/doc/manpages.tex
@@ -719,8 +719,9 @@ about the session, depending on the following specific options.
the session as edited proofs.
\item[\texttt{-{}-stats}] prints various proofs statistics, as
detailed below.
-\item[\texttt{-{}-tree}] prints the structure of the session as a
- tree in ASCII, as detailed below.
+% OBSOLETE
+% \item[\texttt{-{}-tree}] prints the structure of the session as a
+% tree in ASCII, as detailed below.
\item[\texttt{-{}-print0}] separates the results of the options
\verb|provers| and \verb|--edited-files| by the character number 0
instead of end of line \verb|\n|. That allows you to safely use
@@ -739,36 +740,39 @@ why3 session info --edited-files --print0 vstte12_bfs.mlw | \
\end{description}
-\paragraph{Session Tree}
-
-The hierarchical structure of the session is printed as a tree in
-ASCII. The files, theories, goals are marked with a question mark
-\verb|?|, if they are not verified. A proof is usually said to be
-verified if the proof result is \verb|valid| and the proof is not
-obsolete.
-However here specially we separate these two properties. On
-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|.
-
-For example, here are the session tree produced on the ``hello
-proof'' example of Section~\ref{chap:starting}.
-{\scriptsize
-\begin{verbatim}
-hello_proof---../hello_proof.why?---HelloProof?-+-G3-+-Simplify (1.5.4)?
- | `-Alt-Ergo (0.94)
- |-G2?-+-split_goal?-+-G2.2-+-Simplify (1.5.4)
- | | | `-Alt-Ergo (0.94)
- | | `-G2.1?-+-Coq (8.3pl4)?
- | | |-Simplify (1.5.4)?
- | | `-Alt-Ergo (0.94)?
- | |-Simplify (1.5.4)?
- | `-Alt-Ergo (0.94)?
- `-G1---Simplify (1.5.4)
-\end{verbatim}
-}
+
+% OBSOLETE
+
+% \paragraph{Session Tree}
+
+% The hierarchical structure of the session is printed as a tree in
+% ASCII. The files, theories, goals are marked with a question mark
+% \verb|?|, if they are not verified. A proof is usually said to be
+% verified if the proof result is \verb|valid| and the proof is not
+% obsolete.
+% However here specially we separate these two properties. On
+% 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|.
+
+% For example, here are the session tree produced on the ``hello
+% proof'' example of Section~\ref{chap:starting}.
+% {\scriptsize
+% \begin{verbatim}
+% hello_proof---../hello_proof.why?---HelloProof?-+-G3-+-Simplify (1.5.4)?
+% | `-Alt-Ergo (0.94)
+% |-G2?-+-split_goal?-+-G2.2-+-Simplify (1.5.4)
+% | | | `-Alt-Ergo (0.94)
+% | | `-G2.1?-+-Coq (8.3pl4)?
+% | | |-Simplify (1.5.4)?
+% | | `-Alt-Ergo (0.94)?
+% | |-Simplify (1.5.4)?
+% | `-Alt-Ergo (0.94)?
+% `-G1---Simplify (1.5.4)
+% \end{verbatim}
+% }
\paragraph{Session Statistics}
@@ -794,27 +798,31 @@ For example, here are the session statistics produced on the ``hello
proof'' example of Section~\ref{chap:starting}.
{\footnotesize
\begin{verbatim}
-== Number of goals ==
- total: 5 proved: 3
+== Number of root goals ==
+ total: 3 proved: 2
+
+== Number of sub goals ==
+ total: 2 proved: 1
== Goals not proved ==
+-- file ../hello_proof.why
+-- theory HelloProof
+-- goal G2
- +-- transformation split_goal
- +-- goal G2.1
+ +-- transformation split_goal_right
+ +-- goal G2.0
== Goals proved by only one prover ==
+-- file ../hello_proof.why
+-- theory HelloProof
- +-- goal G1: Simplify (1.5.4) (0.00)
- +-- goal G3: Alt-Ergo (0.94) (0.00)
+ +-- goal G1: Alt-Ergo 0.99.1
+ +-- goal G2
+ +-- transformation split_goal_right
+ +-- goal G2.1: Alt-Ergo 0.99.1
+ +-- goal G3: Alt-Ergo 0.99.1
== Statistics per prover: number of proofs, time (minimum/maximum/average) in seconds ==
- Alt-Ergo (0.94) : 2 0.00 0.00 0.00
- Simplify (1.5.4) : 2 0.00 0.00 0.00
-
-\end{verbatim}
+ Alt-Ergo 0.99.1 : 3 0.00 0.00 0.00
+ \end{verbatim}
}
\subsection{Command \texttt{latex}}
@@ -910,14 +918,14 @@ override this default).
\begin{htmlonly}
\begin{rawhtml}
<h1>Why3 Proof Results for Project "hello_proof"</h1>
-<h2><font color="#FF0000">Theory "HelloProof": not fully verified</font></h2>
-<table border="1"><tr><td colspan="2">Obligations</td><td text-rotation="90">Alt-Ergo (0.94)</td><td text-rotation="90">Coq (8.3pl4)</td><td text-rotation="90">Simplify (1.5.4)</td></td></tr>
-<td bgcolor="#C0FFC0" colspan="2">G1</td><td bgcolor="#E0E0E0">---</td><td bgcolor="#E0E0E0">---</td><td bgcolor="#C0FFC0">0.00</td></tr>
-<td bgcolor="#FF0000" colspan="2">G2</td><td bgcolor="#FF8000">0.00</td><td bgcolor="#E0E0E0">---</td><td bgcolor="#FF8000">0.00</td></tr>
-<tr><td bgcolor="#FF0000" colspan="2">split_goal</td><td bgcolor="#E0E0E0"></td><td bgcolor="#E0E0E0"></td><td bgcolor="#E0E0E0"></td></tr>
-<td rowspan="2"> </td><td bgcolor="#FF0000" colspan="1">1.</td><td bgcolor="#FF8000">0.00</td><td bgcolor="#FF8000">0.43</td><td bgcolor="#FF8000">0.00</td></tr>
-<tr><td bgcolor="#C0FFC0" colspan="1">2.</td><td bgcolor="#C0FFC0">0.00</td><td bgcolor="#E0E0E0">---</td><td bgcolor="#C0FFC0">0.00</td></tr>
-<td bgcolor="#C0FFC0" colspan="2">G3</td><td bgcolor="#C0FFC0">0.00</td><td bgcolor="#E0E0E0">---</td><td bgcolor="#FF8000">0.00</td></tr>
+<h2><span style="color:#FF0000">Theory "hello_proof.HelloProof": not fully verified</span></h2>
+<table border="1" style="border-collapse:collapse"><tr><td colspan="2">Obligations</td><td text-rotation="90">Alt-Ergo 0.99.1</td><td text-rotation="90">Coq 8.7.1</td></tr>
+<tr><td style="background-color:#C0FFC0" colspan="2">G1</td><td style="background-color:#C0FFC0">0.00</td><td style="background-color:#E0E0E0">---</td></tr>
+<tr><td style="background-color:#FF0000" colspan="2">G2</td><td style="background-color:#FF8000">0.00</td><td style="background-color:#E0E0E0">---</td></tr>
+<tr><td style="background-color:#FF0000" colspan="2">split_goal_right</td><td style="background-color:#E0E0E0"></td><td style="background-color:#E0E0E0"></td></tr>
+<tr><td rowspan="2" style="width:1ex"></td><td style="background-color:#FF0000" colspan="1">G2.0</td><td style="background-color:#FF8000">0.00</td><td style="background-color:#FF8000">0.29</td></tr>
+<tr><td style="background-color:#C0FFC0" colspan="1">G2.1</td><td style="background-color:#C0FFC0">0.00</td><td style="background-color:#E0E0E0">---</td></tr>
+<tr><td style="background-color:#C0FFC0" colspan="2">G3</td><td style="background-color:#C0FFC0">0.00</td><td style="background-color:#E0E0E0">---</td></tr>
</table>
\end{rawhtml}
\end{htmlonly}