Commits · 4bfdab0de88488896d826b0f77a8dae3c164a486 · Nils Fitinghoff / why3 · GitLab

Snippets Groups Projects

Jul 12, 2018
- Include generated headers instead of declaring functions on the fly. · 4bfdab0d
  Guillaume Melquiond authored 6 years ago
  4bfdab0d
- Add testing for OCaml 4.07.0. · 74df9fab
  Guillaume Melquiond authored 6 years ago
  74df9fab
Jul 11, 2018
- Attribute model_func does not exist · 973d4e3a
  Sylvain Dailler authored 6 years ago
  
  973d4e3a
- Why3 "bootstrap": · 0da5f41e
  Mário Pereira authored 6 years ago
  0da5f41e
- Remove label model which is redundant with model_trace label. #108 · a67650db
  Sylvain Dailler authored 6 years ago
  
  a67650db
- Multiple "use": multiple module names allowed after "use". For instance: · 6fae2d4a
  Mário Pereira authored 6 years ago
  6fae2d4a
- Coercions: cosmetic · 8681df7d
  Mário Pereira authored 7 years ago
  
  8681df7d
Jul 07, 2018
- confine all notation handling inside Ident · 0fea401c
  Andrei Paskevich authored 7 years ago
  0fea401c
Jul 06, 2018
- update a session · 9fbe2a80
  Andrei Paskevich authored 7 years ago
  
  9fbe2a80
- Merge branch 'non-exhaustive-match-in-pdriver-ml' into 'master' · 6e216d5b
  François Bobot authored 7 years ago
  6e216d5b
Jul 05, 2018
- update OCaml extraction driver re 2242838b · 364edd4b
  Andrei Paskevich authored 7 years ago
  
  364edd4b
- Peano: move division and minmax into separate modules · 2242838b
  Andrei Paskevich authored 7 years ago
  
  2242838b
Jul 04, 2018
- upgrade Alt-Ergo to 2.0.0 where possible · c687def9
  Andrei Paskevich authored 7 years ago
  
  c687def9
- upgrade to Alt-Ergo 2.0.0, CVC4 1.5, Z3 4.6.0, Eprover 2.0 where possible · 5c35938d
  Andrei Paskevich authored 7 years ago
  
  5c35938d
- update obsolete sessions · 2c0ebae6
  Andrei Paskevich authored 7 years ago
  
  2c0ebae6
- stdlib: added witness, mach.matrix, mach.peano, and mach.onetime · 4f8752a6
  Jean-Christophe Filliâtre authored 7 years ago
  4f8752a6
Jul 02, 2018
- Introduction: avoid memoization on local transformations · c8e4dcfc
  Andrei Paskevich authored 7 years ago
  
  c8e4dcfc
- Introduce: reuse the ls/pr of the last introduce_premises · 1c824a64
  Andrei Paskevich authored 7 years ago
  1c824a64
- simplify_trivial_quant removes quantifiers over unused variables · 4b8f1cff
  Andrei Paskevich authored 7 years ago
  
  4b8f1cff
- Matrix: add the pure "update" function for applicative updates · 3a9ea01e
  Andrei Paskevich authored 7 years ago
  
  3a9ea01e
- reoder the error case · dae07f2a
  François Bobot authored 7 years ago
  
  dae07f2a
Jun 28, 2018
- New very simple example: Nistonacci numbers · 05648746
  Claude Marché authored 7 years ago
  
  05648746
- [Makefile] add partial match as error · cd76d043
  François Bobot authored 7 years ago
  cd76d043
- IDE: fix #148 use select_iter instead of selection#select_iter · 30f8256a
  Sylvain Dailler authored 7 years ago
  30f8256a
- split_vc: perform generalize_introduced before splitting · 917cd4c9
  Andrei Paskevich authored 7 years ago
  
  917cd4c9
Jun 27, 2018
- [replay] use alt-ergo 1.30 instead of alt-ergo 2.2.0 · adc66fc1
  François Bobot authored 7 years ago
  
  adc66fc1
- Merge branch 'computer_division_for_master' into 'master' · b5b2add1
  François Bobot authored 7 years ago
  b5b2add1
- [Bench] mccarty f19_pseudorec is not proved · dd3125e9
  François Bobot authored 7 years ago
  dd3125e9
- Merge remote-tracking branch 'origin/master' into computer_division_for_master · 28e84fe8
  François Bobot authored 7 years ago
  
  28e84fe8
- Add in-place variants for wmpn_[lr]shift · 116df251
  Raphaël Rieu-Helft authored 7 years ago
  
  116df251
- Introduction: "generalize_introduced" moves local premises back to the goal · e3cfcd52
  Andrei Paskevich authored 7 years ago
  e3cfcd52
- Lexer: use Strings.has_prefix instead of Filename.remove_extension · d95b50c5
  Andrei Paskevich authored 7 years ago
  
  d95b50c5
- Lexer: avoid using Report on TryWhy3 input (temporary fix for #150) · 3820e3ec
  Andrei Paskevich authored 7 years ago
  
  3820e3ec
- WhyML: admit empty loop bodies (while c do done) · 847b605d
  Andrei Paskevich authored 7 years ago
  
  847b605d
Jun 26, 2018
- TryWhy3: fix the order of tasks in a theory + the copyright years · d82e52b6
  Andrei Paskevich authored 7 years ago
  
  d82e52b6
Jun 25, 2018
- Fix typos. · 5bbc031a
  Guillaume Melquiond authored 7 years ago
  
  5bbc031a
- Fix opam file. · 3d4dc823
  Guillaume Melquiond authored 7 years ago
  
  3d4dc823
- New release. · e112153a
  Guillaume Melquiond authored 7 years ago
  
  e112153a
- Add missing headers. · ac9f96ec
  Guillaume Melquiond authored 7 years ago
  
  ac9f96ec
- Clean release notes. · 05de6964
  Guillaume Melquiond authored 7 years ago
  
  05de6964