Commits · f9b19a9707dc71eae23bff6ca825857291094dee · Why3 / why3

21 Aug, 2014 2 commits
- Remove broken obsolete rule. · f9b19a97
  Guillaume Melquiond authored Aug 21, 2014
  
  f9b19a97
- Use definitions for min and max, assuming the relation is a total order. · f535480f
  Guillaume Melquiond authored Aug 21, 2014
  
  f535480f
20 Aug, 2014 1 commit
- fix API doc · 33ececbc
  MARCHE Claude authored Aug 20, 2014
  
  33ececbc
19 Aug, 2014 3 commits
- headers · e29e3119
  MARCHE Claude authored Aug 19, 2014
  
  e29e3119
- src/mlw: start gently the next revision of WhyML · c686e51b
  Andrei Paskevich authored Aug 19, 2014
  
  c686e51b
- transf compute: use a more general reduction engine · 41bd968f
  MARCHE Claude authored Aug 19, 2014
  
  41bd968f
18 Aug, 2014 1 commit
- transformation "compute" · 4f5f81f0
  MARCHE Claude authored Aug 18, 2014
  
  4f5f81f0
08 Aug, 2014 1 commit

make driver/ independent of parser/ · dfda5336

Andrei Paskevich authored Aug 08, 2014

- move common lexing functions to util/lexlib.mll
- move and rename Typing.create_user_tv to Ty.tv_of_string

dfda5336

27 Jul, 2014 1 commit
- Makefile: ln -r is not supported everywhere · 0503c1dd
  Andrei Paskevich authored Jul 27, 2014
  
  0503c1dd
26 Jul, 2014 2 commits
- move why3config to src/tools/ · 3f3fda73
  Andrei Paskevich authored Jul 26, 2014
  
  3f3fda73
- remove why3bench and comparison, subsumed by why3session bench · 4d584469
  Andrei Paskevich authored Jul 22, 2014
  
  4d584469
11 Jul, 2014 2 commits
- move Args inside Whyconf · 96cfbb62
  Andrei Paskevich authored Jul 11, 2014
  
  96cfbb62
- Makefile: separate why3 from why3contraption · 03277cb2
  Andrei Paskevich authored Jul 11, 2014
  
  03277cb2
06 Jul, 2014 1 commit
- Remove conflict noise. · 62e56c3b
  Guillaume Melquiond authored Jul 06, 2014
  
  62e56c3b
29 Jun, 2014 1 commit
- no need for DATADIR/why3/emacs · 0d2ea48d
  MARCHE Claude authored Jun 29, 2014
  
  0d2ea48d
28 Jun, 2014 3 commits
- remove temporary shape files created by tutorial example · 2ce79f5a
  MARCHE Claude authored Jun 28, 2014
  
  2ce79f5a
- resolve conflicts · 441471f5
  MARCHE Claude authored Jun 28, 2014
  
  441471f5
- adding support for compressed files. Needs splitting the library into · da6022c4
  MARCHE Claude authored Jun 27, 2014
```
two parts: why3 and why3session.

(The Coq tactic does not include why3session)
```
  da6022c4
27 Jun, 2014 3 commits
- fix missing backslash · 957b8118
  MARCHE Claude authored Jun 27, 2014
  
  957b8118
- Make sure the link to why3extract is available before running the bench. · bf5879a0
  Guillaume Melquiond authored Jun 27, 2014
  
  bf5879a0
- [Isabelle] fix message when not building heap · d9bffa2b
  MARCHE Claude authored Jun 27, 2014
  
  d9bffa2b
26 Jun, 2014 1 commit
- Fix obsolete calling convention. · 2d7031b5
  Guillaume Melquiond authored Jun 26, 2014
  
  2d7031b5
24 Jun, 2014 2 commits
- better handling of Isabelle compilation of realizations · b70d841b
  MARCHE Claude authored Jun 24, 2014
  
  b70d841b
- temporarily disabled isabelle compilation while there are missing realizations · 1a90fee3
  MARCHE Claude authored Jun 24, 2014
  
  1a90fee3
23 Jun, 2014 1 commit
- pulled Stefan Berghofer changes · 13a4a598
  MARCHE Claude authored Jun 23, 2014
  
  13a4a598
16 Jun, 2014 1 commit
- Change why3replayer into why3replay, so as to match other commands. · f44ea070
  Guillaume Melquiond authored Jun 16, 2014
  
  f44ea070
02 Jun, 2014 1 commit
- Add a why3execute command. · 3631ec9d
  Guillaume Melquiond authored Jun 02, 2014
  
  3631ec9d
28 May, 2014 4 commits
- Add an extract command to why3. · c8efbc1d
  Guillaume Melquiond authored May 28, 2014
  
  c8efbc1d
- Partly adapt the bench to the new commands. · f466ece0
  Guillaume Melquiond authored May 28, 2014
  
  f466ece0
- Make --realize into a proper subcommand. · ff1c023b
  Guillaume Melquiond authored May 28, 2014
  
  ff1c023b
- Factor option parsing for why3 commands. · 9deea655
  Guillaume Melquiond authored May 28, 2014
  
  9deea655
27 May, 2014 2 commits
- Add a "prove" subcommand. · 74e9e7b3
  Guillaume Melquiond authored May 27, 2014
  
  74e9e7b3
- Give a git-like invocation to why3 tools. · eedc2f21
  Guillaume Melquiond authored May 27, 2014
  
  eedc2f21
15 May, 2014 1 commit

Use the supported invocation of AC_INIT. · 4b8b9981

Guillaume Melquiond authored May 15, 2014

The 1-argument version of AC_INIT is obsolete since 2003. Moreover, it
prevents ./configure --version from giving a meaningful output.

4b8b9981

13 May, 2014 5 commits
- Sanitize the Makefile · 0aa124de
  Jacques-Pascal Deplaix authored May 12, 2014 and Jean-Christophe Filliâtre committed May 13, 2014
  
  0aa124de
- Add an uninstall rule · 06354810
  Jacques-Pascal Deplaix authored May 07, 2014 and Jean-Christophe Filliâtre committed May 13, 2014
  
  06354810
- Fix the clean_old_install Makefile rule · abf380d6
  Jacques-Pascal Deplaix authored May 07, 2014 and Jean-Christophe Filliâtre committed May 13, 2014
  
  abf380d6
- Install the emacs mode at the right place · cfc383cb
  Jacques-Pascal Deplaix authored May 06, 2014 and Jean-Christophe Filliâtre committed May 13, 2014
  
  cfc383cb
- Compile the emacs mode if emacs is available · acc138fc
  Jacques-Pascal Deplaix authored May 06, 2014 and Jean-Christophe Filliâtre committed May 13, 2014
  
  acc138fc
23 Apr, 2014 1 commit
- Factorize most of BigInt nums versus zarith · c67a3b49
  MARCHE Claude authored Apr 24, 2014
  
  c67a3b49