- 17 Apr, 2010 4 commits
-
-
Andrei Paskevich authored
-
Andrei Paskevich authored
-
Andrei Paskevich authored
-
Andrei Paskevich authored
- 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
-
- 16 Apr, 2010 1 commit
-
-
MARCHE Claude authored
-
- 10 Apr, 2010 1 commit
-
-
MARCHE Claude authored
-
- 09 Apr, 2010 6 commits
-
-
MARCHE Claude authored
-
Jean-Christophe Filliâtre authored
-
Jean-Christophe Filliâtre authored
-
Francois Bobot authored
-
Francois Bobot authored
-
MARCHE Claude authored
-
- 08 Apr, 2010 3 commits
-
-
MARCHE Claude authored
-
Francois Bobot authored
-
Jean-Christophe Filliâtre authored
-
- 07 Apr, 2010 7 commits
-
-
MARCHE Claude authored
-
MARCHE Claude authored
-
Jean-Christophe Filliâtre authored
No commit message
-
Jean-Christophe Filliâtre authored
-
Jean-Christophe Filliâtre authored
-
Jean-Christophe Filliâtre authored
-
Jean-Christophe Filliâtre authored
-
- 06 Apr, 2010 2 commits
-
-
Jean-Christophe Filliâtre authored
-
MARCHE Claude authored
-
- 05 Apr, 2010 2 commits
-
-
Andrei Paskevich authored
-
Andrei Paskevich authored
default actions in case explicit options are missing. The command line has the following structure: why [options] [[file|-] [-t <theory> [-g <goal>]...]...]... Summary: Qualified theories come from the library, not from file. When the driver is not specified, pretty-print theories. When neither --prove nor --output are given, print tasks. When no theory is specified for a file, use every theory. When no goal is specified for a theory, use every goal. Examples: % why.opt [shows usage information] % why.opt test.why [prints the contents of test.why] % why.opt -t int.Int [prints the library theory int.Int] % why.opt -D drivers/z3.drv test.why [sends every task from test.why to stdout] % why.opt -D drivers/z3.drv -o directory test.why [creates ./directory/ if it's does not exist and sends every task to a separate file in ./directory/] % why.opt -D drivers/z3.drv --prove test.why -t ThA [calls the prover for every goal from theory ThA in test.why] % why.opt -D drivers/z3.drv --prove test.why -t ThA -g G1 -g G2 [calls the prover for G1 and G2 from theory ThA in test.why] % why.opt -D drivers/z3.drv -t int.Abs -g G1 test.why -t ThA [prints G1 from int.Abs and every goal from ThA in test.why]
-
- 03 Apr, 2010 2 commits
-
-
Jean-Christophe Filliâtre authored
-
Jean-Christophe Filliâtre authored
-
- 02 Apr, 2010 2 commits
-
-
MARCHE Claude authored
-
MARCHE Claude authored
-
- 31 Mar, 2010 1 commit
-
-
MARCHE Claude authored
-
- 29 Mar, 2010 2 commits
-
-
MARCHE Claude authored
-
MARCHE Claude authored
-
- 28 Mar, 2010 1 commit
-
-
Andrei Paskevich authored
-
- 27 Mar, 2010 3 commits
-
-
Andrei Paskevich authored
move this implementation to eliminate_let. - initial commit of eliminate_definition : the goal is to translate definitions by match into series of axioms.
-
Andrei Paskevich authored
-
Andrei Paskevich authored
-
- 26 Mar, 2010 3 commits
-
-
MARCHE Claude authored
-
MARCHE Claude authored
-
MARCHE Claude authored
-