Commits · 245166e9c75f675363b39eb66d7bb3e0eb0b0aa7 · Why3 / why3

29 Aug, 2014 7 commits
- Remove why3contraption. · 245166e9
  Guillaume Melquiond authored Aug 29, 2014
  
  245166e9
- Fix typo. · 82d39309
  Guillaume Melquiond authored Aug 29, 2014
  
  82d39309
- Add a clean-coq rule for removing .vo files of realizations. · 718e8fba
  Guillaume Melquiond authored Aug 29, 2014
  
  718e8fba
- fixed default strategies (now written using the strategy syntax) · 7135c146
  Jean-Christophe Filliâtre authored Aug 29, 2014
  
  7135c146
- why3doc: ignore space in blank lines · 47e059dc
  Jean-Christophe Filliâtre authored Aug 29, 2014
  
  47e059dc
- add headers to the new files · 49c520cf
  Andrei Paskevich authored Aug 29, 2014
  
  49c520cf
- bring camlzip into coq-tactic · 28c8b0ff
  Andrei Paskevich authored Aug 29, 2014
```
and merge the why3 and why3session libraries back into one.
```
  28c8b0ff
28 Aug, 2014 8 commits
- added strategies 'Split' and 'Inline' · 89556a91
  Jean-Christophe Filliâtre authored Aug 28, 2014
  
  89556a91
- strategies: added a default label 'exit' · 8affab1b
  Jean-Christophe Filliâtre authored Aug 28, 2014
  
  8affab1b
- update session with isabelle 2014 · b57744eb
  MARCHE Claude authored Aug 28, 2014
  
  b57744eb
- missing shapes · 4ca754c2
  MARCHE Claude authored Aug 28, 2014
  
  4ca754c2
- quicksort: shuffle is implemented *and used* · 86fcfc25
  Jean-Christophe Filliâtre authored Aug 28, 2014
  
  86fcfc25
- Support for Isabelle2014 and Coq8.4pl4 · ddbfb32a
  MARCHE Claude authored Aug 28, 2014
  
  ddbfb32a
- Adapted to Isabelle2014 · 735bf89c
  Stefan Berghofer authored Aug 06, 2014
  
  735bf89c
- Tiny parser for strategies · a94b5657
  Jean-Christophe Filliâtre authored Aug 28, 2014
```
A simple, assembly-like syntax for strategies is introduced.
The code for a strategy is now a single string, in the field
'code' of a 'strategy' entry of a configuration file.
See share/strategies.conf for examples.
```
  a94b5657
27 Aug, 2014 4 commits
- update session · e5442abb
  MARCHE Claude authored Aug 27, 2014
  
  e5442abb
- make message on theory checksums only a debug message · 0c6fbaaa
  MARCHE Claude authored Aug 27, 2014
  
  0c6fbaaa
- fixed XML pretty-printer · 4f54cdeb
  Jean-Christophe Filliâtre authored Aug 27, 2014
  
  4f54cdeb
- linear probing: WIP · 0fdec8a4
  Jean-Christophe Filliâtre authored Jul 04, 2014
  
  0fdec8a4
26 Aug, 2014 10 commits
- remove incorrect test · ea45fdf6
  MARCHE Claude authored Aug 26, 2014
  
  ea45fdf6
- checksums on theories in sessions · 33cbb2d8
  MARCHE Claude authored Aug 26, 2014
  
  33cbb2d8
- a few more simple examples and tests · 1a8008ea
  MARCHE Claude authored Aug 26, 2014
  
  1a8008ea
- updated sessions · c4bcf6a2
  MARCHE Claude authored Aug 26, 2014
  
  c4bcf6a2
- make bench should removed generated why3shapes.gz · 74fae80b
  MARCHE Claude authored Aug 26, 2014
  
  74fae80b
- simple examples and tests · 2325f49a
  MARCHE Claude authored Aug 26, 2014
  
  2325f49a
- compute_in_goal as a strategy · 5d5daeba
  MARCHE Claude authored Aug 26, 2014
  
  5d5daeba
- another blaster, who kills quicksort.mlw in one shot · 309ca235
  MARCHE Claude authored Aug 26, 2014
  
  309ca235
- fixed computation of checksums for theories · 91b04286
  MARCHE Claude authored Aug 26, 2014
  
  91b04286
- protect some exception catching with not Debug.stack_trace · 4ed9a14d
  MARCHE Claude authored Aug 26, 2014
  
  4ed9a14d
25 Aug, 2014 11 commits
- selects the naive pairing algorithm when shapes are not on disk · e76c9a52
  MARCHE Claude authored Aug 25, 2014
  
  e76c9a52
- more informative info messages · 4f881830
  MARCHE Claude authored Aug 25, 2014
  
  4f881830
- Merge branch 'master' of git+ssh://scm.gforge.inria.fr//gitroot/why3/why3 · 7b26666e
  Martin Clochard authored Aug 25, 2014
  
  7b26666e
- (WIP) mini-compiler in Why3 · 5a29d871
  Martin Clochard authored Aug 25, 2014
  
  5a29d871
- allow loading more strategies using --extra-config · 83bb8b95
  MARCHE Claude authored Aug 25, 2014
  
  83bb8b95
- (WIP) mini-compiler proof in progress · 43b24a6b
  Léon Gondelman authored Aug 25, 2014
  
  43b24a6b
- poor man's attempt to compute a checksum for a theory (indeed a miserable failure) · 05c13646
  MARCHE Claude authored Aug 25, 2014
  
  05c13646
- filename for uncompressed shapes should be without extension · be1a46e4
  MARCHE Claude authored Aug 25, 2014
  
  be1a46e4
- session files: preserve prover ids when saving new session · df0b3ef5
  MARCHE Claude authored Aug 25, 2014
  
  df0b3ef5
- install-lib should also install why3session.{cma|cmxa} · 5eb6143e
  MARCHE Claude authored Aug 25, 2014
  
  5eb6143e
- ROADMAP: instructions for OPAM package · 6df23b0b
  MARCHE Claude authored Aug 25, 2014
  
  6df23b0b