aboutsummaryrefslogtreecommitdiffstats
path: root/flocq
Commit message (Collapse)AuthorAgeFilesLines
* Vendored Flocq library: address Coq 8.14 warningXavier Leroy2021-10-031-1/+1
|
* Update the vendored Flocq library to version 3.4.2Xavier Leroy2021-09-254-38/+20
| | | | For compatibility with the upcoming Coq 8.14.
* Replace `omega` tactic with `lia`Xavier Leroy2020-12-291-1/+1
| | | | | | | | | | | Since Coq 8.12, `omega` is flagged as deprecated and scheduled for removal. Also replace CompCert's homemade tactics `omegaContradiction`, `xomega`, and `xomegaContradiction` with `lia` and `extlia`. Turn back on the deprecation warning for uses of `omega`. Make the proof of `Ctypes.sizeof_pos` more robust to variations in `lia`.
* Update Flocq to 3.4.0 (#383)Guillaume Melquiond2020-12-2829-638/+1840
|
* Add FMA (fused multiply-add)Xavier Leroy2019-07-171-0/+121
| | | | | Cherry-pick of the following commit on upstream Flocq: https://gitlab.inria.fr/flocq/flocq/commit/28cc6ee3a278878f3df002aab64a6b93e9412d34
* Make scripts compatible with new behavior of field_simplify (#291)Vincent Laporte2019-05-062-3/+3
| | | | | | | | The `field_simplify` tactics will be improved soon (https://github.com/coq/coq/pull/9854). Flocq was made compatible with this improvement (https://gitlab.inria.fr/flocq/flocq/commit/0752761a6a344d62f6bc728eac442ebb4ba655ac). This commit updates CompCert's copy of Flocq accordingly.
* Upgrade embedded version of Flocq to 3.1.Guillaume Melquiond2019-03-2735-7394/+9493
| | | | | | | | | | | | 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).
* flocq: minor cleaning (#257)Vincent Laporte2018-09-141-3/+2
| | | | | | This change avoids relying on generated names, making the proof script compatible with ongoing evolutions of the `zify` tactic. A similar cleanup was already performed in Flocq's master sources.
* Upgrade Flocq to version 2.6.1 from upstream (#71)Xavier Leroy2018-04-257-171/+420
| | | | | | | | | | | | | | | | 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.
* Change Implicit Arguments to Arguments (#225)Jasper Hugunin2018-03-284-14/+14
| | | | | | | 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.
* Don't depend on the judgmental behavior of Bool.eqb (#217)Jason Gross2018-01-171-1/+1
| | | | | This change is backwards compatible, and makes flocq compatible with https://github.com/coq/coq/pull/6596. Was applied to the Flocq master sources https://gitlab.inria.fr/flocq/flocq/commit/db356aa5ea0fd0234e3872f70e8972086055cd57
* Adapt proofs to future handling of literal constants in Coq.Guillaume Melquiond2017-03-0814-145/+119
| | | | | | This commit is mainly a squash of the relevant compatibility commits from Flocq's master. Most of the changes are meant to make the proofs oblivious to the way constants such as 0, 1, 2, and -1 are represented.
* Update Flocq to version 2.5.2Xavier Leroy2017-02-138-132/+91
| | | | This version of Flocq is compatible with Coq 8.6
* The contradiction tactic has become more powerful.Maxime Dénès2017-01-091-2/+1
|
* Intro patterns have changed semantics...Maxime Dénès2017-01-091-0/+1
|
* 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.5.0.Guillaume Melquiond2015-09-2220-1078/+2444
| | | | Note: this version of Flocq is compatible with both Coq 8.4 and 8.5.
* Upgrade to flocq 2.4.0Jacques-Henri Jourdan2014-10-0717-646/+5920
|
* Update commentxleroy2014-08-131-2/+1
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2562 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Merge of "newspilling" branch:xleroy2014-07-231-0/+51
| | | | | | | | | | | | | | | - Support single-precision floats as first-class values - Introduce chunks Many32, Many64 and types Tany32, Tany64 to support saving and restoring registers without knowing the exact types (int/single/float) of their contents, just their sizes. - Memory model: generalize the opaque encoding of pointers to apply to any value, not just pointers, if chunks Many32/Many64 are selected. - More properties of FP arithmetic proved. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2537 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Merge of Flocq version 2.2.0.xleroy2013-08-0229-223/+1908
| | | | | | | More precise modeling of NaNs. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2303 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Flocq-based parsing of floating-point literals (Jacques-Henri Jourdan)xleroy2012-11-031-4/+4
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2065 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Use Flocq for floatsxleroy2012-06-2828-0/+17154
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1939 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
generated by cgit (git 2.34.1) at 2024-05-09 05:06:11 +0000