Commits · e294f64d4debc919c664a287edf0bd1f73da6e91 · Why3 / why3

13 May, 2011 1 commit
- programs: refactoring of typing (in progress) · 74cded5f
  Jean-Christophe Filliâtre authored May 13, 2011
  
  74cded5f
11 May, 2011 1 commit
- programs: one module = three theories · 9f981b82
  Jean-Christophe Filliâtre authored May 10, 2011
  
  9f981b82
09 May, 2011 1 commit
- programs: regions in progress · 084f446e
  Jean-Christophe Filliâtre authored May 09, 2011
  
  084f446e
15 Feb, 2011 1 commit
- syntax for record type declarations · e3f2f52f
  Jean-Christophe Filliâtre authored Feb 15, 2011
  
  e3f2f52f
25 Jan, 2011 1 commit
- ghost code · 3919a48a
  Jean-Christophe Filliâtre authored Jan 25, 2011
  
  3919a48a
23 Jan, 2011 1 commit
- programs: abstract types · 6e11c32e
  Jean-Christophe Filliâtre authored Jan 23, 2011
  
  6e11c32e
22 Jan, 2011 1 commit
- programs: fixed typing bug · 3ed11623
  Jean-Christophe Filliâtre authored Jan 22, 2011
  
  3ed11623
11 Jan, 2011 1 commit
- programs: fixed benchmarks; cleaning up typing · b1efe700
  Jean-Christophe authored Jan 11, 2011
  
  b1efe700
05 Jan, 2011 1 commit
- programs: a better pretty-printer, for debugging purposes · 30b2bf6b
  Jean-Christophe Filliâtre authored Jan 05, 2011
  
  30b2bf6b
02 Jan, 2011 1 commit
- programs: typing programs first, then annotations · b67464fe
  Jean-Christophe Filliâtre authored Jan 02, 2011
  
  b67464fe
30 Dec, 2010 2 commits
- porting programs to mutable types · 10d709b6
  Jean-Christophe Filliâtre authored Dec 30, 2010
  
  10d709b6
- programs: builtin exn type, variants with inlined lt_nat · 0532d853
  Jean-Christophe Filliâtre authored Dec 30, 2010
  
  0532d853
29 Dec, 2010 2 commits
- programs are now parsed with src/parser/ · 6a159d62
  Jean-Christophe Filliâtre authored Dec 29, 2010
  
  6a159d62
- programs in progress (references -> mutable types) · 8e5ef36a
  Jean-Christophe Filliâtre authored Dec 29, 2010
  
  8e5ef36a
23 Dec, 2010 2 commits
- getting rid of old references · 25c60aa1
  Jean-Christophe Filliâtre authored Dec 23, 2010
  
  25c60aa1
- modules: huge refactoring of programs types, in preparation for mutable types · 72a36bd8
  Jean-Christophe Filliâtre authored Dec 23, 2010
  
  72a36bd8
14 Dec, 2010 1 commit
- mutables types (work in progress) · 2d519b26
  Jean-Christophe Filliâtre authored Dec 14, 2010
  
  2d519b26
13 Dec, 2010 1 commit
- syntax for mutable types · 4d64ac97
  Jean-Christophe Filliâtre authored Dec 13, 2010
  
  4d64ac97
10 Dec, 2010 3 commits
- Env: added a retrieve_channel capability, for use in programs · 9cd84f51
  Jean-Christophe Filliâtre authored Dec 10, 2010
  
  9cd84f51
- program typing now uses modules · 53fce77f
  Jean-Christophe Filliâtre authored Dec 08, 2010
  
  53fce77f
- added new files for modules · 2d22d313
  Jean-Christophe Filliâtre authored Dec 08, 2010
  
  2d22d313
24 Jun, 2010 1 commit
- programs: Pgm_types renamed into Pgm_env; the main control flow is now in Pgm_main.type_and_wp · a49e7de5
  Jean-Christophe Filliâtre authored Jun 24, 2010
  
  a49e7de5
23 Jun, 2010 1 commit
- programs: new type-checker still in progress · 7b1638e1
  Jean-Christophe Filliâtre authored Jun 23, 2010
  
  7b1638e1
22 Jun, 2010 1 commit

programs: complete rewrite of the type-checker in progress (in particular,... · 11fb9f0a

Jean-Christophe Filliâtre authored Jun 22, 2010

programs: complete rewrite of the type-checker in progress (in particular, types dterm and dfmla have been moved to Denv, together with some functions); make does not compile whyml anymore; make bench will stop at the first program test; with my apologies if I messed up somewhere...

11fb9f0a

30 May, 2010 1 commit
- programs: loops, exceptions (in progress) · 83c85fdc
  Jean-Christophe Filliâtre authored May 30, 2010
  
  83c85fdc
28 May, 2010 1 commit
- programs: fixed bug in WP · ec3b9459
  Jean-Christophe Filliâtre authored May 28, 2010
  
  ec3b9459
27 May, 2010 1 commit
- format boxes src/printer/tptp.ml · ed8085c2
  Jean-Christophe Filliâtre authored May 27, 2010
  
  ed8085c2
26 May, 2010 1 commit
- programs: WP for function application and let-in · 84ab8931
  Jean-Christophe Filliâtre authored May 26, 2010
  
  84ab8931
25 May, 2010 2 commits
- programs: ref and := are no more in the theory programs.Prelude, but predefined (in the code) · 5d83cd19
  Jean-Christophe Filliâtre authored May 25, 2010
  
  5d83cd19
- programs: more efficient access to pre-defined symbols; typing is now... · afd48213
  Jean-Christophe Filliâtre authored May 25, 2010
```
programs: more efficient access to pre-defined symbols; typing is now state-less (to be re-entrant, if necessary)
```
  afd48213