- 05 Mar, 2014 4 commits
-
-
Jean-Christophe Filliâtre authored
-
Jean-Christophe Filliâtre authored
-
MARCHE Claude authored
-
MARCHE Claude authored
-
- 04 Mar, 2014 10 commits
-
-
MARCHE Claude authored
-
MARCHE Claude authored
-
MARCHE Claude authored
-
MARCHE Claude authored
-
Guillaume Melquiond authored
-
Guillaume Melquiond authored
-
Guillaume Melquiond authored
-
Jean-Christophe Filliâtre authored
-
MARCHE Claude authored
-
MARCHE Claude authored
-
- 03 Mar, 2014 1 commit
-
-
Jean-Christophe Filliâtre authored
-
- 28 Feb, 2014 2 commits
-
-
Jean-Christophe Filliâtre authored
-
Jean-Christophe Filliâtre authored
-
- 27 Feb, 2014 4 commits
-
-
Jean-Christophe Filliâtre authored
-
MARCHE Claude authored
-
Jean-Christophe Filliâtre authored
support for 31/32/63/64-bit integers in extracted code
-
Jean-Christophe Filliâtre authored
-
- 26 Feb, 2014 3 commits
-
-
Jean-Christophe Filliâtre authored
-
Jean-Christophe Filliâtre authored
All files are extracted to the target repository, even those corresponding to files from the Why3 standard library. Some of these files may be empty (e.g. ref__Ref.ml) when everything is overridden by the OCaml driver. You can ignore these files when compiling the extracted OCaml code.
-
Jean-Christophe Filliâtre authored
-
- 25 Feb, 2014 4 commits
-
-
Jean-Christophe Filliâtre authored
everything is contained in the driver (ocaml.drv) with possible references to OCaml modules contained in why3extract.cma (currently why3__Prelude, why3__BigInt, why3__Map)
-
Jean-Christophe Filliâtre authored
-
Jean-Christophe Filliâtre authored
in particular, consistency of ArrayPermut is now ensured
-
Jean-Christophe Filliâtre authored
-
- 24 Feb, 2014 2 commits
-
-
Jean-Christophe Filliâtre authored
-
Jean-Christophe Filliâtre authored
(that is, using number of occurrences) No more definition of permutation using inductive predicates. Impacts array.ArrayPermut; proof sessions updated. Coq realizations for map.Occ and map.MapPermut; proof session for array.ArrayPermut in progress
-
- 23 Feb, 2014 1 commit
-
-
MARCHE Claude authored
-
- 21 Feb, 2014 5 commits
-
-
MARCHE Claude authored
-
MARCHE Claude authored
-
MARCHE Claude authored
-
MARCHE Claude authored
Problem: lambda is not extracted into a fun ... -> ...
-
MARCHE Claude authored
-
- 20 Feb, 2014 2 commits
-
-
Léon Gondelman authored
-
Jean-Christophe Filliâtre authored
-
- 19 Feb, 2014 2 commits
-
-
Jean-Christophe Filliâtre authored
-
Jean-Christophe Filliâtre authored
-