- 27 Feb, 2015 1 commit
-
-
Guillaume Melquiond authored
-
- 16 Feb, 2015 1 commit
-
-
Guillaume Melquiond authored
-
- 14 Jan, 2015 1 commit
-
-
MARCHE Claude authored
-
- 11 Jan, 2015 2 commits
-
-
MARCHE Claude authored
-
MARCHE Claude authored
-
- 06 Jan, 2015 1 commit
-
-
MARCHE Claude authored
-
- 20 Sep, 2014 1 commit
-
-
Andrei Paskevich authored
-
- 06 Sep, 2014 2 commits
-
-
Andrei Paskevich authored
-
Andrei Paskevich authored
-
- 05 Sep, 2014 1 commit
-
-
Andrei Paskevich authored
-
- 31 Aug, 2014 1 commit
-
-
MARCHE Claude authored
-
- 29 Aug, 2014 1 commit
-
-
Guillaume Melquiond authored
-
- 28 Aug, 2014 1 commit
-
-
Jean-Christophe Filliâtre authored
A simple, assembly-like syntax for strategies is introduced. The code for a strategy is now a single string, in the field 'code' of a 'strategy' entry of a configuration file. See share/strategies.conf for examples.
-
- 08 Aug, 2014 1 commit
-
-
Andrei Paskevich authored
- move common lexing functions to util/lexlib.mll - move and rename Typing.create_user_tv to Ty.tv_of_string
-
- 28 Jun, 2014 1 commit
-
-
MARCHE Claude authored
two parts: why3 and why3session. (The Coq tactic does not include why3session)
-
- 23 Jun, 2014 1 commit
-
-
MARCHE Claude authored
-
- 16 Jun, 2014 1 commit
-
-
Guillaume Melquiond authored
-
- 02 Jun, 2014 1 commit
-
-
Guillaume Melquiond authored
-
- 28 May, 2014 2 commits
-
-
Guillaume Melquiond authored
-
Guillaume Melquiond authored
-
- 27 May, 2014 2 commits
-
-
Guillaume Melquiond authored
-
Guillaume Melquiond authored
-
- 13 May, 2014 1 commit
-
-
- 11 May, 2014 1 commit
-
-
MARCHE Claude authored
-
- 02 May, 2014 1 commit
-
-
MARCHE Claude authored
-
- 26 Apr, 2014 2 commits
-
-
MARCHE Claude authored
-
MARCHE Claude authored
-
- 24 Apr, 2014 1 commit
-
-
MARCHE Claude authored
-
- 23 Apr, 2014 1 commit
-
-
MARCHE Claude authored
-
- 30 Mar, 2014 1 commit
-
-
Jean-Christophe Filliâtre authored
counts lines/tokens in Why3 files distinguishes spec (logic declarations and annotations) and code reports the ratio spec/code with command line option -f example: why3wc -f examples/*.mlw see why3wc --help for more details note: why3wc assumes that input files are lexically well-formed it also makes some approximations (switching from spec to code and conversely is only done when there is a blank line in the middle)
-
- 05 Mar, 2014 1 commit
-
-
Jean-Christophe Filliâtre authored
-
- 27 Feb, 2014 1 commit
-
-
Jean-Christophe Filliâtre authored
support for 31/32/63/64-bit integers in extracted code
-
- 23 Feb, 2014 1 commit
-
-
MARCHE Claude authored
-
- 21 Feb, 2014 2 commits
-
-
MARCHE Claude authored
-
MARCHE Claude authored
Problem: lambda is not extracted into a fun ... -> ...
-
- 16 Feb, 2014 2 commits
-
-
Jean-Christophe Filliâtre authored
-
MARCHE Claude authored
-
- 15 Feb, 2014 1 commit
-
-
MARCHE Claude authored
-
- 27 Jan, 2014 1 commit
-
-
Jean-Christophe Filliâtre authored
-
- 10 Dec, 2013 1 commit
-
-
Jean-Christophe Filliâtre authored
-