Commit message (Collapse) | Author | Age | Files | Lines | |
---|---|---|---|---|---|
* | Upgrade Flocq to version 2.6.1 from upstream (#71) | Xavier Leroy | 2018-04-25 | 1 | -2/+0 |
| | | | | | | | | | | | | | | | | We were previously at 2.5.2. Quoting the NEWS from upstream: Version 2.6.1: - ensured compatibility from Coq 8.4 to 8.8 Version 2.6.0: - ensured compatibility from Coq 8.4 to 8.7 - removed some hypotheses on some lemmas of Fcore_ulp - added lemmas to Fprop_plus_error - improved examples Also: in preparation for Coq 8.8, silence warning "compatibility-notation" when building Flocq, because this warning is on by default in 8.8, and Flocq triggers it a lot. | ||||
* | Upgrade to Flocq 2.5.0. | Guillaume Melquiond | 2015-09-22 | 1 | -2/+3 |
| | | | | Note: this version of Flocq is compatible with both Coq 8.4 and 8.5. | ||||
* | Merge of Flocq version 2.2.0. | xleroy | 2013-08-02 | 1 | -2/+2 |
| | | | | | | | More precise modeling of NaNs. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2303 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e | ||||
* | Use Flocq for floats | xleroy | 2012-06-28 | 1 | -0/+237 |
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1939 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e |