GitLab

Makefile: make examples/toto-gallery exports example toto to /users/toccata/filliatr/toccata/web/gallery/

As a side effect, provers-detection-data.conf no longer needs to be preprocessed.

why3 tests/test-eval.why -P alt-ergo -T T --eval c1 --eval c2 --eval c3

in a series of tests on available examples, lightweight polymorphism
encoding techniques combined with a more agressive generation of
monomorphic instances (via Discriminate) show better results than
our earlier defaults.

In the same commit:
- remove Encoding_explicit (unsound), Encoding_decoexp (too naive),
  and Encoding_instantiate (subsumed by Discriminate)
- rename Encoding_decorate to Encoding_tags_full and Encoding_guard
  to Encoding_guards_full
- move Encoding_guards_full specific functions from Libencoding to
  Encoding_guards_full
- do not apply type protection in "encoding_tptp" and remove
  Protect_finite which is not needed anymore.

[GTK sourceview] why.lang renamed to why3.lang

This fixes the bug with .dep cleaning, when we don't build the IDE.

Also, can we merge the replayer into why3session already, please?