GitLab

As they say, "A penny saved is ridiculous."

Why3 library mechanism is not adapted for forward dependencies.

Discard old pieces between Qed and the next blank line, so that generated commands about implicit arguments are not preserved.

Note: Currently, only the set of real theories has been fully converted to
the new script format. So it is the only one enabled. The other ones would
not survive the process.

Make its building rule a bit quieter.

Note: they are stable with respect to the following command.
why3 --realize -D drivers/coq-realize.drv -T toto.Titi -o lib/coq/toto/