Use the actual html generated by why3session rather than an image for the html version of the documentation.

Do not update the proof duration if it changed by less than 10% or 0.1s, so as to avoid diff noise in session files.

The only significant difference between these functions is that the first
one is calling a callback function at each step, while the second one is
generating a report at the end. Any other differences are likely to be
actual bugs, which hopefully are now fixed. Now both functions call a
third one, which accepts callbacks that encompass all the previous
features.

Disclaimer: the code is ugly.

allows to show the warnings in the nightly bench

If the user happens to select all the goals in the IDE and press replay,
a quadratic number of proof attempts are actually scheduled: each goal is
scheduled as many times as it has ancestors. This patch fixes it.

With the previous code, one could start with an original time limit of a
few seconds and end up with proof attempts running for several minutes
after a few unsuccessful tries with provers that are aware of the actual
limit. Now, the actual time limit is never more than twice the user-defined
one.

induction_int_lex : new induction tactic (labels only, no heuristic provided) for ordered int tuples.

this is an experimental feature, not yet proved, not yet tested.
Currently, it is only used when a debug flag "implicit_post" is set.
It might need some tweaking to work well with booleans.