Commits · 3e5bad9c8fcb9022f17ee243839f697588d940a8 · Flocq / flocq

18 Oct, 2010 3 commits
- Restored axpy compilation. · 3e5bad9c
  Guillaume Melquiond authored Oct 18, 2010
  
  3e5bad9c
- Release 1.0. · b727623a
  Guillaume Melquiond authored Oct 18, 2010
  
  b727623a
- Renamed generic_*_pt into round_*_pt. · 2e9b95b4
  Guillaume Melquiond authored Oct 18, 2010
  
  2e9b95b4
15 Oct, 2010 3 commits
- Used Z -> bool for choice function of rounding to nearest. · f63e1f7b
  Guillaume Melquiond authored Oct 15, 2010
  
  f63e1f7b
- Added rewriting rules for Zle_bool. · 4a3af0f6
  Guillaume Melquiond authored Oct 15, 2010
  
  4a3af0f6
- Added Zaway function. · c9056dfa
  Guillaume Melquiond authored Oct 15, 2010
  
  c9056dfa
12 Oct, 2010 2 commits
- Simplified proof. · a86c150e
  Guillaume Melquiond authored Oct 12, 2010
  
  a86c150e
- Added generic_ZR_pt. · 401b2cc8
  Guillaume Melquiond authored Oct 12, 2010
  
  401b2cc8
11 Oct, 2010 4 commits
- Added generic_NA_pt. · c00ca01c
  Guillaume Melquiond authored Oct 11, 2010
  
  c00ca01c
- Added round_N_middle. · 948cba2c
  Guillaume Melquiond authored Oct 11, 2010
  
  948cba2c
- Added Rnd_NA_N_pt. · bb8e0d1e
  Guillaume Melquiond authored Oct 11, 2010
  
  bb8e0d1e
- Added Rplsu_eq_reg_r. · c5fa19c8
  Guillaume Melquiond authored Oct 11, 2010
  
  c5fa19c8
07 Oct, 2010 6 commits
- Avoided _aux theorems. · f3c3f037
  Guillaume Melquiond authored Oct 07, 2010
  
  f3c3f037
- Simplified proof. · 4964a0d0
  Guillaume Melquiond authored Oct 07, 2010
  
  4964a0d0
- Reduced dependencies of Fprop_plup_error. Marked lemmas as such and fixed comment. · 4bb89f65
  Guillaume Melquiond authored Oct 07, 2010
  
  4bb89f65
- Reduced dependencies of Fprop_Sterbenz. · 24cf49f7
  Guillaume Melquiond authored Oct 07, 2010
  
  24cf49f7
- Merged Fcalc_round_FIX into Fcalc_round. · 948f1e3b
  Guillaume Melquiond authored Oct 07, 2010
  
  948f1e3b
- Moved rounding-specific theorems to Fcalc_round in order to reduce dependencies. · 23d52e14
  Guillaume Melquiond authored Oct 07, 2010
  
  23d52e14
06 Oct, 2010 11 commits
- Added comments on the Calc part of the libary. · 7d4d7827
  Guillaume Melquiond authored Oct 06, 2010
  
  7d4d7827
- Split bpow_le and bpow_lt into implication theorems. · 1965172b
  Guillaume Melquiond authored Oct 06, 2010
  
  1965172b
- Modified Makefile to create all the html files · ec812f45
  BOLDO Sylvie authored Oct 06, 2010
  
  ec812f45
- Moved Rmin_compare. · 8841d22e
  Guillaume Melquiond authored Oct 06, 2010
  
  8841d22e
- Added instance of Fsqrt as an example. · 71242001
  Guillaume Melquiond authored Oct 06, 2010
  
  71242001
- Used not_FTZ_prop. · 5a58abf3
  Guillaume Melquiond authored Oct 06, 2010
  
  5a58abf3
- Renamed theorems. · 53df9d8b
  Guillaume Melquiond authored Oct 06, 2010
  
  53df9d8b
- Removed MonotoneP, IdempotentP, Rounding_for_Format. · 5f48113c
  Guillaume Melquiond authored Oct 06, 2010
  
  5f48113c
- Comments again · 02047e05
  BOLDO Sylvie authored Oct 06, 2010
  
  02047e05
- Comments · 69e7e659
  BOLDO Sylvie authored Oct 06, 2010
  
  69e7e659
- Comments · 5742a158
  BOLDO Sylvie authored Oct 06, 2010
  
  5742a158
05 Oct, 2010 2 commits
- More comments (and used by coqdoc) · a90ca0c2
  BOLDO Sylvie authored Oct 05, 2010
  
  a90ca0c2
- Changed name for rounding to zero. · aac8298e
  Guillaume Melquiond authored Oct 05, 2010
  
  aac8298e
04 Oct, 2010 1 commit
- At least ! le_pred_lt finished... · 99e7d2b9
  BOLDO Sylvie authored Oct 04, 2010
  
  99e7d2b9
01 Oct, 2010 6 commits
- Added Appli as installed directory. · bcc03886
  Guillaume Melquiond authored Oct 01, 2010
  
  bcc03886
- Added license banner to the .v files. · ec58e33a
  Guillaume Melquiond authored Oct 01, 2010
  
  ec58e33a
- Added COPYING file. · b574e6b5
  Guillaume Melquiond authored Oct 01, 2010
  
  b574e6b5
- Changed some theorem names. · 4aa79696
  Guillaume Melquiond authored Oct 01, 2010
  
  4aa79696
- Added implicit coercions for radix and ln_beta. · 81b2a74c
  Guillaume Melquiond authored Oct 01, 2010
  
  81b2a74c
- WIP pred(x) · fb5135b4
  BOLDO Sylvie authored Oct 01, 2010
  
  fb5135b4
29 Sep, 2010 2 commits
- Still about pred · 750219e4
  BOLDO Sylvie authored Sep 29, 2010
  
  750219e4
- rounding_DN_pred · f26588e6
  BOLDO Sylvie authored Sep 29, 2010
  
  f26588e6