Commits · master · Flocq / flocq

13 Jul, 2022 1 commit
- Ensure compatibility with Coq's PR 16293. · 3c92e3f9
  Guillaume Melquiond authored Jul 13, 2022
  
  3c92e3f9
28 Apr, 2022 1 commit
- New release. · 0188199c
  Guillaume Melquiond authored Apr 26, 2022
  
  0188199c
27 Apr, 2022 2 commits
- Properly handle the compatibility files. · 445ea0ff
  Guillaume Melquiond authored Apr 27, 2022
  
  445ea0ff
- Merge branch 'flocq-3' · c96f0422
  Guillaume Melquiond authored Apr 27, 2022
  
  c96f0422
26 Apr, 2022 1 commit
- Remove the BSN alias, as it confuses Coq's extraction mechanism. · 0fc92743
  Guillaume Melquiond authored Apr 26, 2022
  
  0fc92743
15 Apr, 2022 7 commits
- Merge branch 'flocq-3' · d648041e
  Guillaume Melquiond authored Apr 15, 2022
  
  d648041e
- Add Bnearbyint and Btrunc. · 5510a80f
  Paul Geneau authored Apr 15, 2022 and Guillaume Melquiond committed Apr 15, 2022
  
  5510a80f
- Prove inbetween_float_NA_sign. · ec7ea911
  Paul Geneau authored Apr 15, 2022 and Guillaume Melquiond committed Apr 15, 2022
  
  ec7ea911
- Prove Zdigits_succ_le. · cdcd92b7
  Paul Geneau authored Apr 15, 2022 and Guillaume Melquiond committed Apr 15, 2022
  
  cdcd92b7
- Prove Rlt_bool_cond_Ropp. · 1d5cf2ac
  Paul Geneau authored Apr 15, 2022 and Guillaume Melquiond committed Apr 15, 2022
  
  1d5cf2ac
- Prove Ztrunc_div. · e81ae57d
  Paul Geneau authored Apr 15, 2022 and Guillaume Melquiond committed Apr 15, 2022
  
  e81ae57d
- Prove cond_Zopp_0. · 87af079a
  Paul Geneau authored Apr 14, 2022 and Guillaume Melquiond committed Apr 15, 2022
  
  87af079a
14 Apr, 2022 1 commit
- Update CI. · 81ec26b3
  Guillaume Melquiond authored Apr 14, 2022
  
  81ec26b3
01 Mar, 2022 2 commits
- Merge branch 'coq_15754' into 'flocq-3' · 792f4a3a
  Guillaume Melquiond authored Mar 01, 2022
```
Adapt to https://github.com/coq/coq/pull/15754

See merge request !19
```
  792f4a3a
- Adapt to https://github.com/coq/coq/pull/15754 · ef9d501a
  Pierre Roux authored Mar 01, 2022
  
  ef9d501a
17 Feb, 2022 2 commits
- Remove some compatibility lemmas. · 5a9d2d34
  Guillaume Melquiond authored Feb 17, 2022
  
  5a9d2d34
- Simplify proofs a bit. · 3af469f4
  Guillaume Melquiond authored Feb 16, 2022
  
  3af469f4
16 Feb, 2022 6 commits
- Prove Beqb_refl. · ef12d4a7
  Guillaume Melquiond authored Feb 16, 2022
  
  ef12d4a7
- Fix compilation issues. · 56addf5c
  Guillaume Melquiond authored Feb 16, 2022
  
  56addf5c
- Change check-more so that it compiles files using the installed libraries. · 55e006e4
  Guillaume Melquiond authored Feb 16, 2022
  
  55e006e4
- Clean proof. · 32db7151
  Guillaume Melquiond authored Feb 16, 2022
  
  32db7151
- Add helper canonical_bounded. · cc5372fb
  Guillaume Melquiond authored Feb 16, 2022
  
  cc5372fb
- Relate canonical exponent and order. · 44236b02
  Guillaume Melquiond authored Feb 16, 2022
  
  44236b02
14 Feb, 2022 1 commit
- Improve compatibility with Coq 8.16. · c81b1f10
  Guillaume Melquiond authored Feb 14, 2022
  
  c81b1f10
17 Jan, 2022 2 commits
- Merge branch 'flocq-3' · a8de4a9c
  Guillaume Melquiond authored Jan 17, 2022
  
  a8de4a9c
- New release. · 088acf93
  Guillaume Melquiond authored Jan 17, 2022
  
  088acf93
19 Nov, 2021 1 commit
- Merge branch 'print17' into 'master' · 1423a6d3
  Guillaume Melquiond authored Nov 19, 2021
```
Decimal printing of binary64 with 17 digits is enough

See merge request !18
```
  1423a6d3
13 Nov, 2021 1 commit
- Decimal printing of binary64 with 17 digits is enough · 09d83571
  Pierre Roux authored Nov 12, 2021
  
  09d83571
09 Nov, 2021 1 commit
- Compatibility with Coq 8.15. · e68658cb
  Kazuhiko Sakaguchi authored Nov 05, 2021 and Guillaume Melquiond committed Nov 09, 2021
  
  e68658cb
05 Nov, 2021 3 commits
- New release. · 311182de
  Guillaume Melquiond authored Nov 05, 2021
  
  311182de
- Compatibility with Coq 8.15. · b8652003
  Kazuhiko Sakaguchi authored Nov 05, 2021 and Guillaume Melquiond committed Nov 05, 2021
  
  b8652003
- Clean code a bit. · 4a37ff45
  Guillaume Melquiond authored Nov 05, 2021
  
  4a37ff45
03 Nov, 2021 5 commits
- Remove INR from Pff. · 117c4d0a
  Guillaume Melquiond authored Nov 03, 2021
```
This commit also cleans real literals.
```
  117c4d0a
- Update Coq versions. · 7a697420
  Guillaume Melquiond authored Nov 03, 2021
  
  7a697420
- Merge branch 'flocq-3' · 138f34bf
  Guillaume Melquiond authored Nov 03, 2021
  
  138f34bf
- Silence warning. · dc95fa7f
  Guillaume Melquiond authored Nov 03, 2021
  
  dc95fa7f
- Add a rule to install .glob files (fix #19 ). · d26acf9f
  Guillaume Melquiond authored Nov 03, 2021
  
  d26acf9f
27 Sep, 2021 1 commit
- Silence warning (fix #18 ). · b20cb064
  Xavier Leroy authored Sep 27, 2021 and Guillaume Melquiond committed Sep 27, 2021
  
  b20cb064
01 Sep, 2021 1 commit
- Adapt to coq/coq#14819 · a40e7487
  Pierre Roux authored Sep 01, 2021
  
  a40e7487
28 Jun, 2021 1 commit
- New release. · ca655d25
  Guillaume Melquiond authored Jun 28, 2021
  
  ca655d25