- 28 Apr, 2010 5 commits
-
-
Andrei Paskevich authored
-
Andrei Paskevich authored
- move compile_match to Eliminate_algebraic - move eliminate_builtin to Eliminate_definition
-
Andrei Paskevich authored
-
Andrei Paskevich authored
-
Jean-Christophe Filliâtre authored
-
- 27 Apr, 2010 1 commit
-
-
Andrei Paskevich authored
-
- 26 Apr, 2010 13 commits
-
-
Andrei Paskevich authored
-
Andrei Paskevich authored
-
Andrei Paskevich authored
-
Andrei Paskevich authored
-
Andrei Paskevich authored
-
Andrei Paskevich authored
-
Andrei Paskevich authored
-
Andrei Paskevich authored
-
Francois Bobot authored
-
Andrei Paskevich authored
-
Andrei Paskevich authored
-
Francois Bobot authored
-
Francois Bobot authored
Pour que l'on donne toujours les mêmes déclarations pour le type à encoder dans plusieurs taches différentes
-
- 25 Apr, 2010 14 commits
-
-
Andrei Paskevich authored
-
Andrei Paskevich authored
- use simplifying constructors in "eliminate_definition"
-
Andrei Paskevich authored
I will always compile before committing I will always compile before committing I will...
-
Andrei Paskevich authored
-
Andrei Paskevich authored
like f_map_sign should only be applied from specialized recursive functions and these funcitons will usually supply the polarity argument.
-
Andrei Paskevich authored
In particular, it is now independent of compile_match.
-
Andrei Paskevich authored
-
Andrei Paskevich authored
-
Andrei Paskevich authored
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.
-
Andrei Paskevich authored
-
Francois Bobot authored
-
Andrei Paskevich authored
-
Francois Bobot authored
-
Francois Bobot authored
-
- 24 Apr, 2010 2 commits
-
-
Francois Bobot authored
-
Andrei Paskevich authored
-
- 23 Apr, 2010 5 commits
-
-
Francois Bobot authored
printer : print_prelude inside printers instead of prover.ml. Required for smt which has its own prelude.
-
Andrei Paskevich authored
-
Andrei Paskevich authored
If this works, it will be a less intrusive way to get dependencies right, than to use lib/why.mli.
-
MARCHE Claude authored
-
Francois Bobot authored
amelioration(hack) du makefile pour que malgré le pack les dependances vers why soient bonnes, why.cma why.cmxa sont construit dans lib
-