Commits · 28106e2c7d806dc742d437e6d6b3edc8aae738b8 · Why3 / why3

17 Jul, 2012 1 commit
- updated all proof sessions with the new shape algorithm · 28106e2c
  MARCHE Claude authored Jul 17, 2012
  
  28106e2c
16 Jul, 2012 17 commits
- whyml: one-step variant for algebraic types · 52ff6ba0
  Andrei Paskevich authored Jul 16, 2012
  
  52ff6ba0
- support multiple variants in WhyML syntax · ea3729f4
  Andrei Paskevich authored Jul 16, 2012
  
  ea3729f4
- whyml: minor optimization · 72b30954
  Andrei Paskevich authored Jul 16, 2012
  
  72b30954
- whyml: several API simplifications · 9b75e276
  Andrei Paskevich authored Jul 16, 2012
```
- get rid of val_decl, the psymbol/pvsymbol is enough
- get rid of vtv_vars, keep the varset in pvsymbol
- include fresh regions in pd_news (will serve for clone)
```
  9b75e276
- updated proof session for decease1 · 89294b25
  Jean-Christophe Filliâtre authored Jul 16, 2012
  
  89294b25
- new shape version · c33b1457
  MARCHE Claude authored Jul 16, 2012
  
  c33b1457
- pvs: silence OCaml warning · bcbcd870
  Andrei Paskevich authored Jul 16, 2012
  
  bcbcd870
- Fix default intros for Coq: type parameters were missing · df8265b4
  MARCHE Claude authored Jul 16, 2012
  
  df8265b4
- update proofs for examples/programs/hash_tables · fa8007b4
  Andrei Paskevich authored Jul 16, 2012
  
  fa8007b4
- show exceptions raised by introduce_premises in gmain · 4766b5dd
  Andrei Paskevich authored Jul 16, 2012
  
  4766b5dd
- treat polymorphic goals correctly in introduce_premises · 8dd4a931
  Andrei Paskevich authored Jul 16, 2012
  
  8dd4a931
- update session for blocking_semantics2 · 1627eb07
  MARCHE Claude authored Jul 16, 2012
  
  1627eb07
- session: add optional "format" attribute for <file> · 487d866f
  Andrei Paskevich authored Jul 16, 2012
  
  487d866f
- IDE: reorganize debug output · b0c5c8d7
  Andrei Paskevich authored Jul 16, 2012
  
  b0c5c8d7
- update proofs · 75871d67
  Asma Tafat-Bouzid authored Jul 16, 2012
  
  75871d67
- update obsolete sessions · 9127530d
  MARCHE Claude authored Jul 16, 2012
  
  9127530d
- example blocking semantic · e5e241c0
  Asma Tafat-Bouzid authored Jul 16, 2012
  
  e5e241c0
15 Jul, 2012 1 commit
- update session for shapshottable_trees · bdb05c5e
  Andrei Paskevich authored Jul 15, 2012
  
  bdb05c5e
14 Jul, 2012 12 commits
- core: protect the symbol_map type · 6ad7c409
  Andrei Paskevich authored Jul 14, 2012
  
  6ad7c409
- whyml: admit restricted forms of partial application · b54d03f2
  Andrei Paskevich authored Jul 14, 2012
  
  b54d03f2
- whyml: provide a builtin module for %Exit · 0c11fc9a
  Andrei Paskevich authored Jul 14, 2012
  
  0c11fc9a
- make programs in the gallery compatible with whyml · 63d89abb
  Andrei Paskevich authored Jul 14, 2012
  
  63d89abb
- whyml: distinguish "let" and "let rec" in pretty-printing · ec869ddc
  Andrei Paskevich authored Jul 14, 2012
  
  ec869ddc
- make standard library modules compatible with whyml · 2fceb267
  Andrei Paskevich authored Jul 14, 2012
  
  2fceb267
- whyml: refresh unmodified subregions in abstract parameters · 05583b01
  Andrei Paskevich authored Jul 14, 2012
  
  05583b01
- whyml: fix Mlw_expr.eff_check · 16351b6f
  Andrei Paskevich authored Jul 14, 2012
  
  16351b6f
- whyml: private types · da42c225
  Andrei Paskevich authored Jul 14, 2012
  
  da42c225
- whyml: uncovered exceptions have postcondition "true" · 5760e7db
  Andrei Paskevich authored Jul 14, 2012
  
  5760e7db
- whyml: accept "naked" effects on external variables · 50c6d499
  Andrei Paskevich authored Jul 14, 2012
  
  50c6d499
- PVS realizations · a8057f6f
  Jean-Christophe Filliâtre authored Jul 14, 2012
  
  a8057f6f
13 Jul, 2012 9 commits
- whyml: minor changes · 324c1fb3
  Andrei Paskevich authored Jul 14, 2012
  
  324c1fb3
- blocking semantic · e75ceeba
  Asma Tafat-Bouzid authored Jul 13, 2012
  
  e75ceeba
- session: enable debugging output in the pairing code · 28fac8bc
  Andrei Paskevich authored Jul 13, 2012
  
  28fac8bc
- whyml: use the same variable order as Pgm_wp · 39100a92
  Andrei Paskevich authored Jul 13, 2012
  
  39100a92
- blocking semantic · 83404088
  Asma Tafat-Bouzid authored Jul 13, 2012
  
  83404088
- blocking semantic · 80c69550
  Asma Tafat-Bouzid authored Jul 13, 2012
  
  80c69550
- blocking semantic (proofs) · ad56b76e
  Asma Tafat-Bouzid authored Jul 13, 2012
  
  ad56b76e
- let whyml-exp use the old session files · 9577acb9
  Andrei Paskevich authored Jul 13, 2012
  
  9577acb9
- whyml: fix drop_at · 96a33ff8
  Andrei Paskevich authored Jul 13, 2012
  
  96a33ff8