aboutsummaryrefslogtreecommitdiffstats
path: root/flocq/Calc
Commit message (Collapse)AuthorAgeFilesLines
* Update Flocq to 3.4.0 (#383)Guillaume Melquiond2020-12-285-46/+55
|
* Upgrade embedded version of Flocq to 3.1.Guillaume Melquiond2019-03-278-809/+759
| | | | | | | | | | | | Main changes to CompCert outside of Flocq are as follows: - Minimal supported version of Coq is now 8.7, due to Flocq requirements. - Most modifications are due to Z2R being dropped in favor of IZR and to the way Flocq now handles NaNs. - CompCert now correctly handles NaNs for the Risc-V architecture (hopefully).
* Change Implicit Arguments to Arguments (#225)Jasper Hugunin2018-03-281-1/+1
| | | | | | | Implicit Arguments is deprecated in Coq since 8.6 or so. Some Implicit Arguments remained in Flocq but were recently changed to Arguments. Apply the same change to our local copy of Flocq. As a positive consequence, we no longer need to suppress the deprecation warnings while compiling Flocq.
* Update Flocq to version 2.5.2Xavier Leroy2017-02-131-1/+2
| | | | This version of Flocq is compatible with Coq 8.6
* Port to Coq 8.5pl2Xavier Leroy2016-07-081-1/+1
| | | | | Manual merging of branch jhjourdan:coq8.5. No other change un functionality.
* Upgrade to flocq 2.4.0Jacques-Henri Jourdan2014-10-074-436/+17
|
* Merge of Flocq version 2.2.0.xleroy2013-08-026-12/+12
| | | | | | | 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 floatsxleroy2012-06-286-0/+2835
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1939 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e