aboutsummaryrefslogtreecommitdiffstats
path: root/lib/Floats.v
Commit message (Expand)AuthorAgeFilesLines
* Values: conversions to nearest intDavid Monniaux2021-12-121-0/+9
* _ne conversionsDavid Monniaux2021-12-121-0/+9
* Merge branch 'master' of https://github.com/AbsInt/CompCert into towards_3.10David Monniaux2021-09-241-0/+1
|\
| * Avoid `Global Set Asymmetric Patterns` (#408)Xavier Leroy2021-09-151-0/+1
| * Use the LGPL instead of the GPL for dual-licensed filesXavier Leroy2021-05-081-4/+5
* | [BROKEN] Merge with v3.9 : something broken for __builtin_expect in cfrontend...Cyril SIX2021-06-011-4/+5
* | Merge branch 'master' into merge_master_8.13.1Sylvain Boulmé2021-03-231-105/+105
|\|
| * Replace `omega` tactic with `lia`Xavier Leroy2020-12-291-105/+105
| * Remove useless parameters in theorems int_round_odd_bits and int_round_odd_leXavier Leroy2020-12-291-8/+8
* | Merge branch 'master' (Absint 3.8) into kvx-work-merge3.8David Monniaux2020-11-181-2/+2
|\|
| * Support the use of already-installed MenhirLib and Flocq librariesXavier Leroy2020-09-211-2/+1
| * Import ListNotations explicitlyXavier Leroy2020-05-041-0/+1
| * Revert "Do not use the list notation `[]`"Xavier Leroy2020-05-041-8/+8
| * Do not use the list notation `[]`Xavier Leroy2020-05-041-8/+8
* | Ibuiltin proofCyril SIX2019-10-041-1/+62
|/
* Coq 8.10 compatibility: make explicit the "core" hint databaseXavier Leroy2019-08-051-2/+2
* Another way to derive floatofintu from floatofintXavier Leroy2019-07-171-0/+41
* Add floating-point square root and fused multiply-addXavier Leroy2019-07-171-3/+51
* Revised specification of NaN payload behaviorXavier Leroy2019-07-121-124/+104
* Avoid relying on `Export` bug (#301)Maxime Dénès2019-07-041-1/+2
* Rename Fappli_IEEE_extra.v into IEEE754_extra.vXavier Leroy2019-04-261-1/+1
* Move Z definitions out of Integers and into ZbitsXavier Leroy2019-04-261-4/+3
* lib/Coqlib.v: remove defns about multiplication, division, modulusXavier Leroy2019-04-231-2/+2
* Floats.v: remove leftover Print commandsXavier Leroy2019-04-041-5/+1
* Floats.v: avoid using module Zlogarithm in the proofsXavier Leroy2019-04-031-10/+19
* Upgrade embedded version of Flocq to 3.1.Guillaume Melquiond2019-03-271-143/+163
* Add functions "ordered" and "compare" to Float and Float32Xavier Leroy2018-12-201-9/+20
* Remove coq warnings (#28)Bernhard Schommer2017-09-221-17/+17
* Hybrid 64bit/32bit PowerPC portBernhard Schommer2017-05-031-0/+69
* Port to Coq 8.5pl2Xavier Leroy2016-07-081-12/+9
* Updated PR by removing whitespaces. Bug 17450.Bernhard Schommer2015-10-201-134/+134
* Tighten and prove correct the underflow/overflow bounds for parsing of FP lit...Xavier Leroy2015-07-061-96/+2
* build_from_parsed: simplified code + correctness proof.Xavier Leroy2014-11-151-15/+86
* Upgrade to flocq 2.4.0Jacques-Henri Jourdan2014-10-071-87/+94
* The NaN behavior of float_of_single differs on PowerPC and on IA32/ARM.xleroy2014-07-281-73/+18
* Merge of "newspilling" branch:xleroy2014-07-231-1466/+1016
* Add Proof keyword so that documentation generation worksjjourdan2014-07-041-0/+2
* floatoflong_from_words, floatoflongu_from_words : proof of PowerPc implementa...jjourdan2014-03-131-89/+316
* floatoflong_decomp, floatoflongu_decompjjourdan2014-03-111-0/+238
* Introduce and use the platform-specific Archi module giving:xleroy2014-01-031-7/+6
* Floats.v, Nan.v: hard-wire the general shape of binop_pl, so that no axioms xleroy2013-09-141-21/+119
* Merge of Flocq version 2.2.0.xleroy2013-08-021-105/+339
* More accurate model of condition register flags for ARM and IA32.xleroy2013-07-131-0/+6
* Revised handling of int->float conversions:xleroy2013-07-081-3/+81
* Treat casts int64 -> float32 as primitive operations instead of twoxleroy2013-07-031-0/+18
* Merge of the float32 branch: xleroy2013-05-191-0/+28
* Big merge of the newregalloc-int64 branch. Lots of changes in two directions:xleroy2013-04-201-44/+28
* Glasnost: making transparent a number of definitions that were opaquexleroy2013-03-101-0/+1
* Updated PowerPC port to new integers.xleroy2013-02-121-1/+2
* lib/Integers.v: revised and extended, faster implementation based onxleroy2013-02-101-33/+29
generated by cgit (git 2.34.1) at 2024-05-09 02:49:41 +0000