GitLab

small fix for neq pretty-printing bug

code is still quite ugly, and more testing is required

simplify_trivial_quantifier va moins sous les triggers (il peut encore remplacer dessous mais pas y trouver d'égalité)

use of why AST in progress for tptp2why, but building a theory still does not work

It should build without problems

(exists x. x=t and F) -> F[t/x]
(forall x. x<>t or F) -> F[t/x]

Cette transformation n'élimine pas les quantifications qui ont des
triggers mais s'applique sous ces derniers. Le but est de pouvoir
éliminer les quantifications inutilement ajoutées lors de eliminate
inductive.

No commit message

why AST and pretty-printing facilities
implementation not yet complete

-I option to specify include dir

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

Now it needs testing.

indentation is still incorrect

improvements in parsing/lexing for tptp2why
output is being converted to why format (not finished yet)