Commits · ba6df492e2017e641d3e5a0baf379b0aa35dd0f4 · Nils Fitinghoff / why3 · GitLab

Snippets Groups Projects

Sep 23, 2018
- bench: ring_decision is moved to in_progress · ba6df492
  Andrei Paskevich authored 6 years ago
  
  ba6df492
- move ring_decision to in_progress/ · 0693e41b
  Andrei Paskevich authored 6 years ago
  
  0693e41b
- update the shapes to v5 in regtests · 1de56fdb
  Andrei Paskevich authored 6 years ago
  1de56fdb
- update some obsolete sessions · 149c9bd9
  Andrei Paskevich authored 6 years ago
  
  149c9bd9
- remove trivial goals from sessions · bbd2dc4d
  Andrei Paskevich authored 6 years ago
  
  bbd2dc4d
Sep 21, 2018
- Extraction: minor · 558c5423
  Mário Pereira authored 6 years ago
  
  558c5423
- Vc: avoid generating trivial VCs · fc1d0588
  Andrei Paskevich authored 6 years ago
  
  fc1d0588
- Vc: another attempt at (slightly) improving termination checking · 017f3334
  Andrei Paskevich authored 6 years ago
  
  017f3334
Sep 20, 2018
- Merge branch '185_let_premise_apply' into 'master' · 22eea516
  DAILLER Sylvain authored 6 years ago
  22eea516
- [transform apply] let is now a premise for applied condition of apply · 35ffacad
  Sylvain Dailler authored 6 years ago
  
  35ffacad
Sep 18, 2018
- Stdlib/floats: allow the use of basic float operations in programs · 58a3584f
  Claude Marché authored 6 years ago
  
  58a3584f
- ce bench: recover examples jlamp0 · 442bffc9
  Sylvain Dailler authored 6 years ago
  
  442bffc9
Sep 14, 2018
- Merge branch 'for_framac' into 'master' · 3c35856d
  François Bobot authored 6 years ago
  3c35856d
- [Transform] Abstract quantifier abstract also quantifiers in goal · 7fc3d39c
  François Bobot authored 6 years ago
  
  7fc3d39c
- [Coq] Remove a SearchAbout · 2891ec49
  François Bobot authored 7 years ago
  
  2891ec49
- Install for_drivers coq realization · 4ba8aea9
  François Bobot authored 7 years ago
  
  4ba8aea9
- Make pinning the git repository work · 7de7991f
  François Bobot authored 7 years ago
  
  7de7991f
- Fix obsoleted sessions · e259438a
  Raphaël Rieu-Helft authored 6 years ago
  
  e259438a
- Remove dead code. · b43e3c1d
  Guillaume Melquiond authored 6 years ago
  
  b43e3c1d
Sep 13, 2018
- Revert "Vc: slight improvement for identical terms in termination checking" · 2b5ecd47
  Guillaume Melquiond authored 6 years ago
  2b5ecd47
- Add support for coercions in "if" and "match" (fix issue #35). · 68effd14
  Guillaume Melquiond authored 6 years ago
  
  68effd14
- Vc: minor · 55e8f989
  Andrei Paskevich authored 6 years ago
  
  55e8f989
- Vc: slight improvement for identical terms in termination checking · ce0b3584
  Andrei Paskevich authored 6 years ago
  
  ce0b3584
- Update .mailmap file. · 9b6c6b38
  Guillaume Melquiond authored 6 years ago
  
  9b6c6b38
- Give a default ordering to range types (fix issue #56). · c78bbf45
  Guillaume Melquiond authored 6 years ago
  
  c78bbf45
- Make --flat option meaningful. · 72d90c94
  Guillaume Melquiond authored 6 years ago
  
  72d90c94
- Extraction: fixed extraction of ghost branchs in [try..with] expressions; · 5e080086
  Mário Pereira authored 6 years ago
  5e080086
Sep 12, 2018
- a few more proofs of stdlib pigeon · 74cda38e
  Claude Marché authored 6 years ago
  
  74cda38e
- Improve the lexicographic order for variants. · 0fb980c6
  Guillaume Melquiond authored 6 years ago
  0fb980c6
- Clean examples. · 250deb85
  Guillaume Melquiond authored 6 years ago
  
  250deb85
Sep 11, 2018
- Add a few more examples to continuous integration. · 1f4ad208
  Guillaume Melquiond authored 6 years ago
  
  1f4ad208
- Clean prover settings a bit. · f086a68c
  Guillaume Melquiond authored 6 years ago
  
  f086a68c
- Split benches. · f226c87c
  Guillaume Melquiond authored 6 years ago
  
  f226c87c
- OCaml printer: pattern priting protected by parentheses. · 47f6a44c
  Mário Pereira authored 6 years ago
  47f6a44c
- Fix a broken session · c7690747
  Raphaël Rieu-Helft authored 6 years ago
  
  c7690747
- Remove handcrafted error messages (fix issues #150 and #172). · ce21b6c1
  Guillaume Melquiond authored 6 years ago
  ce21b6c1
Sep 10, 2018
- Make why3 recognizes the "help" pseudo-command. · 201d8696
  Guillaume Melquiond authored 6 years ago
  201d8696
- Remove obsolete occurrences of "contraption". · c8f1411f
  Guillaume Melquiond authored 6 years ago
  
  c8f1411f
- replay: display the new prover name in case of prover upgrade · 21240a21
  Claude Marché authored 6 years ago
  
  21240a21
- CPU_duplicate policy finally implemented · 935f1d7d
  Claude Marché authored 6 years ago
  
  935f1d7d