aboutsummaryrefslogtreecommitdiffstats
path: root/flocq/Calc/Fcalc_ops.v
Commit message (Collapse)AuthorAgeFilesLines
* 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.
* Upgrade to flocq 2.4.0Jacques-Henri Jourdan2014-10-071-11/+13
|
* Merge of Flocq version 2.2.0.xleroy2013-08-021-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 floatsxleroy2012-06-281-0/+161
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1939 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e