Commits · acc138fc4f42eff2ce15123c43e371834e81aca9 · Why3 / why3

13 May, 2014 4 commits
- 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
- Define and prove mul_limbs. · cc6d1e85
  Guillaume Melquiond authored May 13, 2014
  
  cc6d1e85
- Fix extraction of ocaml32/mach.int.UInt32. · 03d30160
  Guillaume Melquiond authored May 13, 2014
  
  03d30160
- Merge branch 'claude' · 77a7ca18
  MARCHE Claude authored May 13, 2014
  
  77a7ca18
12 May, 2014 5 commits
- Add and prove mul_limb. · 503ddd14
  Guillaume Melquiond authored May 12, 2014
  
  503ddd14
- Improve messages. · 0fac64a3
  Guillaume Melquiond authored May 12, 2014
  
  0fac64a3
- Minor fix in Coq printer. · 9c0d73ef
  Julien Thierry authored May 07, 2014 and Guillaume Melquiond committed May 12, 2014
```
When the proof terminator was missing at the end of a Coq file, Why3
deleted the whole proof. Now Why3 no longer discards the proof
inadvertently.
```
  9c0d73ef
- ocaml driver: better translation of mach.int.Unsigned.zero_unsigned · ab3433fa
  MARCHE Claude authored May 12, 2014
  
  ab3433fa
- Remove broken proof attempts from queens. · 15678f50
  Guillaume Melquiond authored May 12, 2014
  
  15678f50
11 May, 2014 12 commits
- fix typo · 14645424
  MARCHE Claude authored May 11, 2014
  
  14645424
- mp: prepare for multiplication · 700b3079
  MARCHE Claude authored May 11, 2014
  
  700b3079
- Merge branch 'claude' · bb11ac5a
  MARCHE Claude authored May 11, 2014
  
  bb11ac5a
- mp: in place addition, javascript extraction, all proved · 12855fcc
  MARCHE Claude authored May 11, 2014
  
  12855fcc
- mp: extract to javascript · e3332a88
  MARCHE Claude authored May 11, 2014
  
  e3332a88
- mp: extraction to ocaml · 77c67856
  MARCHE Claude authored May 11, 2014
  
  77c67856
- moved addc into mach.int.Unsigned.add_with_carry · 2519704b
  MARCHE Claude authored May 11, 2014
  
  2519704b
- mp: add on type t proved. add_limb remains to be realized · 12106d30
  MARCHE Claude authored May 11, 2014
  
  12106d30
- theory int.Power : one more lemma · 2d539148
  MARCHE Claude authored May 11, 2014
  
  2d539148
- mp: all proved except lemma power_non_neg · b92d65ff
  MARCHE Claude authored May 11, 2014
  
  b92d65ff
- mp: N.add proved modulo some lemmas · ac7ed714
  MARCHE Claude authored May 11, 2014
  
  ac7ed714
- modules mach.array.*: add explanations · 19cb2ee1
  MARCHE Claude authored May 11, 2014
  
  19cb2ee1
09 May, 2014 2 commits
- proof of add in progress · 8a6206c0
  MARCHE Claude authored May 09, 2014
  
  8a6206c0
- new version of multiprecision arithmetic · 8ab8d007
  MARCHE Claude authored May 09, 2014
  
  8ab8d007
07 May, 2014 1 commit
- Remove redundant hypothesis from axioms about set.Fsetint.min/max_elt. · f7b45e7c
  Guillaume Melquiond authored May 07, 2014
  
  f7b45e7c
05 May, 2014 3 commits
- bigInt: compare fully proved, but lemmas remain to prove · 1e1c2f0c
  MARCHE Claude authored May 05, 2014
  
  1e1c2f0c
- bigInt: proof of compare in progress · a733bce4
  MARCHE Claude authored May 05, 2014
  
  a733bce4
- Additional lemma on int.Power.power · b475210f
  MARCHE Claude authored May 05, 2014
  
  b475210f
03 May, 2014 2 commits
- AVL example: README · 6be732cd
  Martin Clochard authored May 03, 2014
  
  6be732cd
- AVL example: Removed some useless arguments. · b551e9d8
  Martin Clochard authored May 03, 2014
  
  b551e9d8
02 May, 2014 11 commits
- Merge branch 'master' into claude · 5432d834
  MARCHE Claude authored May 02, 2014
  
  5432d834
- bigInt: stricter invariant · e0abc171
  MARCHE Claude authored Apr 29, 2014
  
  e0abc171
- bigInt: parsing decimal literals · da874595
  MARCHE Claude authored Apr 27, 2014
  
  da874595
- improved extraction process · 98175d3c
  MARCHE Claude authored Apr 27, 2014
  
  98175d3c
- bigInt: remove leading zeros · f7db94c9
  MARCHE Claude authored Apr 26, 2014
  
  f7db94c9
- bigInt: better test · 80631220
  MARCHE Claude authored Apr 26, 2014
  
  80631220
- bigInt: javascript · a70ac5c1
  MARCHE Claude authored Apr 26, 2014
  
  a70ac5c1
- bigInt: Z.add proved · 1aa814f0
  MARCHE Claude authored Apr 26, 2014
  
  1aa814f0
- bigInt.N.add: fully proved · a6917e6b
  MARCHE Claude authored Apr 26, 2014 and MARCHE Claude committed May 02, 2014
  
  a6917e6b
- bigInt.add: in progress · fd307916
  MARCHE Claude authored Apr 26, 2014 and MARCHE Claude committed May 02, 2014
  
  fd307916
- bigInt: attempt to prove add · a403809b
  MARCHE Claude authored Apr 26, 2014 and MARCHE Claude committed May 02, 2014
  
  a403809b