- 07 Jul, 2010 1 commit
-
-
MARCHE Claude authored
-
- 06 Jul, 2010 11 commits
-
-
Andrei Paskevich authored
(thus, e.g., both alt-ergo and smt printers can register "AC")
-
Andrei Paskevich authored
-
MARCHE Claude authored
-
Jean-Christophe Filliâtre authored
-
Francois Bobot authored
-
Francois Bobot authored
-
Francois Bobot authored
-
Francois Bobot authored
-
Francois Bobot authored
-
Jean-Christophe Filliâtre authored
-
Andrei Paskevich authored
-
- 05 Jul, 2010 11 commits
-
-
Jean-Christophe Filliâtre authored
-
MARCHE Claude authored
-
Jean-Christophe Filliâtre authored
-
Jean-Christophe Filliâtre authored
-
MARCHE Claude authored
-
Jean-Christophe Filliâtre authored
installation (work in progress, currently for developers only); why.conf is also searched for in the installation path (Config.why_libdir); in why.conf, theories and drivers filenames are relative to why.conf dirname (when relative)
-
Jean-Christophe Filliâtre authored
-
MARCHE Claude authored
-
MARCHE Claude authored
-
MARCHE Claude authored
-
Jean-Christophe Filliâtre authored
-
- 04 Jul, 2010 2 commits
-
-
Andrei Paskevich authored
- introduce a new Theory.tdecl "Meta" to be used for tags - simplify cloning procedure, get rid of the th_clone field - when a goal proposition is discarded during cloning, it's still keeped in the theory as a "skip proposition", this is needed to preserve/clone every local identifier. Skip propositions are eliminated during task formation. - get rid of a separate Task.tdecl type - reorganize the Task.task_hd record: * use/clone history is cached in a theory-keyed map; * meta-properties are cached in a tagname-keyed map. This is done to simplify the fine-grained configuration of transformations.
-
Jean-Christophe Filliâtre authored
-
- 02 Jul, 2010 4 commits
-
-
MARCHE Claude authored
-
Jean-Christophe Filliâtre authored
-
Andrei Paskevich authored
-
MARCHE Claude authored
-
- 01 Jul, 2010 1 commit
-
-
Jean-Christophe Filliâtre authored
-
- 29 Jun, 2010 1 commit
-
-
Andrei Paskevich authored
constructor parameters : mainly useful for records, see examples/programs/vacid_0_sparse_array
-
- 28 Jun, 2010 1 commit
-
-
Simon Cruanes authored
now ocamlgraph can be used properly in hypothesis_selection
-
- 26 Jun, 2010 1 commit
-
-
Francois Bobot authored
-
- 25 Jun, 2010 6 commits
-
-
Andrei Paskevich authored
-
Andrei Paskevich authored
-
Jean-Christophe Filliâtre authored
-
Jean-Christophe Filliâtre authored
-
Jean-Christophe Filliâtre authored
-
Jean-Christophe Filliâtre authored
-
- 24 Jun, 2010 1 commit
-
-
Andrei Paskevich authored
in the logic language into (more or less) higher-order style. For example, logic func (x : int, y : int, 'a list) : (int, 'a) map list logic pred (bool, int * real) is now written: logic func (x y : int) (list 'a) : list (map int 'a) logic pred bool (int, real) Note that types use prefix notation (as in Coq) and the types of tuples are now written as (type1, type2, ..., typeN). - Use the same syntax of type expressions in the program language. - Allow binders of the form (x y:int) in the program language.
-