Commits · b1b0f0850f944f59e25553e690ed754ecfc2eac6 · Nils Fitinghoff / why3 · GitLab

Snippets Groups Projects

Nov 03, 2015
- small fix about licenses of icon sets · b1b0f085
  Claude Marché authored 9 years ago
  
  b1b0f085
- Support for PolyPaver prover · b284adfa
  Claude Marché authored 9 years ago
  
  b284adfa
Oct 30, 2015
- IDE: be more robust when displaying VCs whose source file cannot be found · 99d922cd
  Claude Marché authored 9 years ago
  
  99d922cd
Oct 27, 2015
- Merge branch 'counter-examples' · a610b3f7
  David Hauzar authored 9 years ago
  
  a610b3f7
Oct 26, 2015
- Correct lemma permut_refl in theory seq.Permut · aff46e8d
  Mário Pereira authored 9 years ago
  
  aff46e8d
Oct 23, 2015
- Displaying of counterexamples enhanced. · d92706f7
  David Hauzar authored 9 years ago
  d92706f7
- Fixed session for new example rightmostbittrick · f16a2523
  Claude Marché authored 9 years ago
  
  f16a2523
- add rightmostbittrick example · 8a3775ad
  Clément Fumex authored 9 years ago
  
  8a3775ad
Oct 22, 2015
- fixed proofs · eda3dfb6
  Claude Marché authored 9 years ago
  
  eda3dfb6
- example bitwalker: a version of 'peek' closer to SPARK-generated version · 4920bbf3
  Claude Marché authored 9 years ago
  
  4920bbf3
- Bugfix to previous commit. · f7093a76
  David Hauzar authored 9 years ago
  
  f7093a76
- double_wp: fixed session · 735f4968
  Claude Marché authored 9 years ago
  
  735f4968
- Fix of failure in_of_string on Windows. · 34578b05
  David Hauzar authored 9 years ago
  34578b05
Oct 21, 2015
- Schorr-Waite: updated sessions · def4af12
  Mário Pereira authored 9 years ago
  
  def4af12
- New option --extra-expl-prefix to specify other prefixes for VC explanations · c77a1a86
  Claude Marché authored 9 years ago
  
  c77a1a86
- updated sessions · ad518fe0
  Claude Marché authored 9 years ago
  
  ad518fe0
Oct 20, 2015
- simplify_formula: also simplify formula that occurs inside terms · aa0b071b
  Martin Clochard authored 9 years ago
  
  aa0b071b
- eliminate_epsilon: recognize eta-expansions · 1125e975
  Martin Clochard authored 9 years ago
  
  1125e975
Oct 19, 2015
- updated sessions · a120c27e
  Claude Marché authored 9 years ago
  
  a120c27e
- Support for Z3 4.4.0, released on Apr 29, 2015 · a8cfacb5
  Claude Marché authored 9 years ago
  a8cfacb5
- Support for upcoming PolyPaver 0.3 in progress · df70d354
  Claude Marché authored 9 years ago
  df70d354
- updated sessions · 856a2088
  Claude Marché authored 9 years ago
  
  856a2088
- updated sessions · 13d953d2
  Claude Marché authored 9 years ago
  
  13d953d2
- Alt-Ergo: addd option -no-rm-eq-existential to prevent an Alt-Ergo bug · 264805ac
  Claude Marché authored 9 years ago
  
  264805ac
- simplify_trivial_quantification: occurences 'v1 = v2' could not be selected for v2 · d2644f33
  Martin Clochard authored 9 years ago
  
  d2644f33
Oct 17, 2015
- Metitarski, real.Trigonometry: all props removed · 7890825f
  Claude Marché authored 9 years ago
  
  7890825f
Oct 16, 2015
- theory real.Trigonometry: replaced the insanely too precise bounds · 33670484
  Claude Marché authored 9 years ago
  33670484
- In a driver, add the possibility to remove all the locally defined · daf92378
  Clément Fumex authored 9 years ago
  daf92378
- Support for Gappa 1.2.0 · 955ddf6f
  Claude Marché authored 9 years ago
  
  955ddf6f
Oct 14, 2015
- Update Coq proofs of the examples. · 913c316a
  Guillaume Melquiond authored 9 years ago
  
  913c316a
- Merge branch 'master' of git+ssh://scm.gforge.inria.fr/gitroot/why3/why3 · cd56dae7
  Mário Pereira authored 9 years ago
  
  cd56dae7
- Theory seq.ToFset: lemma 'to_set_mem' written using predicate 'mem' for sequences · e33ac290
  Mário Pereira authored 9 years ago
  
  e33ac290
- Do not keep the declaration for "%old". · 5fe2e452
  Guillaume Melquiond authored 9 years ago
  5fe2e452
Oct 13, 2015
- Merge branch 'bugfix/v0.86' · 218e736a
  Guillaume Melquiond authored 9 years ago
  
  218e736a
- Fix hints about symlink creation. · 2fa1b306
  Guillaume Melquiond authored 9 years ago
  
  2fa1b306
- Update opam packages. · d57512a2
  Guillaume Melquiond authored 9 years ago
  
  d57512a2
- Version 0.86.2 · 8f84e5d3
  Guillaume Melquiond authored 9 years ago
  
  8f84e5d3
- Ensure compatibility with Flocq 2.5. · 6236657f
  Guillaume Melquiond authored 9 years ago
  
  6236657f
- Licensing info both in README and in LICENCE · 2f56d736
  Claude Marché authored 9 years ago
  
  2f56d736
- Dterm: admit formulas in let-in (fixes #19565) · c3fcec7b
  Andrei Paskevich authored 9 years ago
  
  c3fcec7b