The old code was assuming that, if lablgtk2 and ocamlfind were installed,
lablgtksourceview2 was installed too. The new code explicitly checks for
both libraries.

Presumably, it won't work correctly if someone has decided to install
lablgtksourceview2 in a different location from lablgtk2, but it wouldn't
have worked with the previous version either, so it isn't a regression.

This allows to call editors from IDE in a less hackish way
and might even fix the problem with Coq editing on Windows.

Suppose that marks appear in order L1, L2, L3 in a program.
Previously, x@L2@L1@L3 would end up with the value of x at mark L1 (the latest mark encountered by WP, that is, the earliest mark in the program).
Now, x@L2@L1@L3 will end up with the value of x at mark L2 (the innermost mark in the expression).

From a WP point of view, the sequence was
x@L2@L1@L3 -> x@L2@L1@now (L3) -> x@L2@L1 (unref) -> x@now@L1 (L2) -> x@now@L1 (unref) -> x@now@now (L1) -> x_L1 (unref).
Now the sequence of substitution is
x@L2@L1@L3 -> x@L2@L1@now (L3) -> x@L2@L1 (unref) -> x@now@L1 (L2) -> x_L2 (unref).

the memlimit parameter is ignored and the timelimit parameter
is still treated as a wallclock time. However, the execution
time shown is the CPU time.

This is only a draft which may not even compile.

Circumvent problem with implicits

the time limit for the replay is the max of the time limit
given initially and twice the time taken by the prover
(if the result was "valid")

E.g, if Alt-Ergo said valid in 4.9 seconds, for an initial limit of 5,
then the replay will give 10 seconds