Commits · 43e979f2d5da98c3037852b23ac0b98ffd9aae14 · Flocq / flocq

13 Jul, 2010 1 commit
- Fixed installation of .vo files into nested directories. · 43e979f2
  Guillaume Melquiond authored Jul 13, 2010
  
  43e979f2
08 Jun, 2010 1 commit
- Added theorems on relative error. · 9bae25bc
  Guillaume Melquiond authored Jun 08, 2010
  
  9bae25bc
31 May, 2010 1 commit
- Proved that the error of addition rounded to nearest is an FP number. · 05352609
  Guillaume Melquiond authored May 31, 2010
  
  05352609
26 May, 2010 2 commits
- Proved that the error of multiplication is an FP number in FLX. · f89097cf
  Guillaume Melquiond authored May 26, 2010
  
  f89097cf
- Added proof of Sterbenz' lemma. · cc1cc5e3
  Guillaume Melquiond authored May 26, 2010
  
  cc1cc5e3
17 May, 2010 7 commits
- Generalized rounding to any exponent function. · ed2f8375
  Guillaume Melquiond authored May 17, 2010
  
  ed2f8375
- Added rounding for FLX formats. · 3b9c00f0
  Guillaume Melquiond authored May 17, 2010
  
  3b9c00f0
- Added rounding for most directions. · 88a7663e
  Guillaume Melquiond authored May 17, 2010
  
  88a7663e
- Added rounding for FIX formats. · aa2b17eb
  Guillaume Melquiond authored May 17, 2010
  
  aa2b17eb
- Added square root algorithm. · 50542867
  Guillaume Melquiond authored May 17, 2010
  
  50542867
- Added division algorithm. · 827cade0
  Guillaume Melquiond authored May 17, 2010
  
  827cade0
- Added function digits for computing the length of a mantissa. · 7ac9a175
  Guillaume Melquiond authored May 17, 2010
  
  7ac9a175
01 Mar, 2010 1 commit
- Added some facts about location and rounding. · ad0188af
  Guillaume Melquiond authored Mar 01, 2010
  
  ad0188af
24 Feb, 2010 2 commits
- Added some new lemmas. Unsuccesfully tried to convert some lemmas from Pff. · 6f68b82d
  Guillaume Melquiond authored Feb 24, 2010
  
  6f68b82d
- Refactored file hierarchy. · 12ff1621
  Guillaume Melquiond authored Feb 24, 2010
  
  12ff1621
02 Oct, 2009 1 commit
- Added concrete addition and multiplication. · 65368b90
  Guillaume Melquiond authored Oct 02, 2009
  
  65368b90
16 Sep, 2009 1 commit
- Added format flushed to zero. · a59e0aa8
  Guillaume Melquiond authored Sep 16, 2009
  
  a59e0aa8
15 Sep, 2009 1 commit
- Started proofs on rounding to nearest even. · 6bbe7159
  Guillaume Melquiond authored Sep 15, 2009
  
  6bbe7159
08 Apr, 2009 1 commit
- Started facts on ulp. · 5e950a10
  Guillaume Melquiond authored Apr 08, 2009
  
  5e950a10
26 Mar, 2009 1 commit
- Added generic rounding. · a0cf797a
  Guillaume Melquiond authored Mar 26, 2009
  
  a0cf797a
20 Mar, 2009 1 commit
- Added missing file. · 6fe105d6
  Guillaume Melquiond authored Mar 20, 2009
  
  6fe105d6
27 Jan, 2009 1 commit
- Split some generic results away. · c7f144ba
  Guillaume Melquiond authored Jan 27, 2009
  
  c7f144ba
26 Jan, 2009 1 commit
- Partial of proof of FLX_format_satisfies_any. · 163e4579
  Guillaume Melquiond authored Jan 26, 2009
  
  163e4579
23 Jan, 2009 1 commit
- Split properties. · 20b97dd0
  Guillaume Melquiond authored Jan 23, 2009
  
  20b97dd0
22 Jan, 2009 1 commit
- Fixed suffix rules. · 05f9af1f
  Guillaume Melquiond authored Jan 22, 2009
  
  05f9af1f
21 Jan, 2009 2 commits
- Fixed automake warning. Cleaned glob files. · 61b4af34
  Guillaume Melquiond authored Jan 21, 2009
  
  61b4af34
- Ensures Coqdep 8.2 works correctly. · efd1c579
  BOLDO Sylvie authored Jan 21, 2009
  
  efd1c579
20 Jan, 2009 2 commits
- Moved verbatim files into src. · c783206e
  Guillaume Melquiond authored Jan 20, 2009
  
  c783206e
- Added some autostuff magic. · dff53855
  Guillaume Melquiond authored Jan 20, 2009
  
  dff53855