| treat correctly the triggers in "eliminate_if" |
|
More...
|
over 15 years ago
|
| in "eliminate_algebraic", use "let" instead of quantifiers, when possible |
|
More...
|
over 15 years ago
|
| Rassemblement de Trans.Error et Printers_utils.Errror en Register.Error |
|
More...
|
over 15 years ago
|
| Pour que l'on donne toujours les mêmes déclarations pour le type à encoder dans plusieurs taches différentes |
|
More...
|
over 15 years ago
|
| add "eliminate_if" to why3_total_elimination.drv |
|
More...
|
over 15 years ago
|
| - make "eliminate_algebraic" polarity-aware - use simplifying constructors in "eliminate_definition" |
|
More...
|
over 15 years ago
|
| I will always compile before committing I will always compile before committing I will always compile before committing I will... |
|
More...
|
over 15 years ago
|
| add f_equ_simp/f_neq_simp + make other simplifications a bit smarter |
|
More...
|
over 15 years ago
|
| do not export f_map_pos and f_map_neg: traversal functions like f_map_sign should only be applied from specialized recursive functions and these funcitons will usually supply the polarity argument. |
|
More...
|
over 15 years ago
|
| remove unnecessary transformations from eliminate_definition. In particular, it is now independent of compile_match. |
|
More...
|
over 15 years ago
|
| bugfix: actual transformation application was accidentally removed |
|
More...
|
over 15 years ago
|
| reject "if-then-else" under "match" in terms |
|
More...
|
over 15 years ago
|
| add "eliminate_if", an alternative (and shorter) implementation of eliminate_ite, based on continuation-passing map. |
|
More...
|
over 15 years ago
|
| add continuation-passing map (useful for complex transformations) |
|
More...
|
over 15 years ago
|
| eliminate if_then_else with sign |
|
More...
|
over 15 years ago
|
| bugfix in Term.f_map_sign (equivalence treatment) |
|
More...
|
over 15 years ago
|
| take care of the sign of the subformula |
|
More...
|
over 15 years ago
|
| eliminate ite and eliminate if_then_else |
|
More...
|
over 15 years ago
|
| ajout d'exception dans printer_utils, utilisation dans alt-ergo et smt |
|
More...
|
over 15 years ago
|
| export print_theory_tdecl in Pretty |
|
More...
|
over 15 years ago
|
| encoding_decorate can use the tag "encoding_decorate : kept" printer : print_prelude inside printers instead of prover.ml. Required for smt which has its own prelude. |
|
More...
|
over 15 years ago
|
| remove lib/ |
|
More...
|
over 15 years ago
|
| trick ocamldep by putting an empty why.ml in src. If this works, it will be a less intrusive way to get dependencies right, than to use lib/why.mli. |
|
More...
|
over 15 years ago
|
| ignore |
|
More...
|
over 15 years ago
|
| amelioration(hack) du makefile pour que malgré le pack les dependances vers why soient bonnes, why.cma why.cmxa sont construit dans lib |
|
More...
|
over 15 years ago
|
| - put back "assert false" in Eliminate_inductive - rewrite Trans.report to stop my eyes bleeding |
|
More...
|
over 15 years ago
|
| ffalse ttrue in util.ml |
|
More...
|
over 15 years ago
|
| inlining driver aware |
|
More...
|
over 15 years ago
|
| Ajout d'exception dans Trans que les transformations doivent utiliser |
|
More...
|
over 15 years ago
|
| respect query_remove in Eliminate_definition |
|
More...
|
over 15 years ago
|
