GitLab

why AST and pretty-printing facilities
implementation not yet complete

corrected infinite loop when menhir does not produce .output file 
for tptp2why target

currently lexing is not operational

The printer exists but is not yet usable.

- move compile_match to Eliminate_algebraic
- move eliminate_builtin to Eliminate_definition

of eliminate_ite, based on continuation-passing map.

François, I don't really intend to redo everything you do, honest!
It's just that I reflected on this solution since Friday and was
too enthralled with it to abandon it.

If this works, it will be a less intrusive way to 
get dependencies right, than to use lib/why.mli.

amelioration(hack) du makefile pour que malgré le pack les dependances vers why soient bonnes, why.cma why.cmxa sont construit dans lib

- no more version.sh, use config.ml.in and version.tex.in instead
- dynlink compatibility is moved to config.ml
- comment out unused sections in Makefile
- provide the explicit --enable-ide option
- provide the explicit --enable-plugins option
- require at least Ocaml 3.10
- remove *-yes and *-no targets from Makefile,
  use ifeq() instead