GitLab

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.

induction tactic: cleaning up (an old version of tactic (induction_ty) is removed). Induction on integers will be fixed soon (actually does not work)

Now, any reference to an external variable in an effect is stored
in a fake variant. This is better than to create a fake exceptional
postcondition, because then Mlw_typing can reject useless xposts.

The empty string is now a recognized configuration filename. It means that
the default configuration with an empty loadpath should be loaded. It also
means it will not be saved.

This removes the need for a WHY3NOCONFIG environment variable and some
tricks based on the WHY3LOADPATH variable. This also removes the need for
a /dev/null file.

and a bit of cleaning at the same time