aboutsummaryrefslogtreecommitdiffstats
path: root/lib/Floats.v
Commit message (Expand)AuthorAgeFilesLines
* 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
* 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
* 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
* Ported to Coq 8.4pl1. Merge of branches/coq-8.4.xleroy2013-01-291-3/+9
* Remove some useless "Require".xleroy2012-12-301-2/+0
* Flocq-based parsing of floating-point literals (Jacques-Henri Jourdan)xleroy2012-11-031-3/+39
* Changelog: updatedxleroy2012-06-281-0/+14
* Use Flocq for floatsxleroy2012-06-281-52/+725
* float->int conversions, continued: weaker axiomatization.xleroy2010-10-291-22/+3
* Float.intoffloat and Float.intuoffloat are now partial functions.xleroy2010-10-281-6/+25
* Merge of the reuse-temps branch:xleroy2010-09-021-17/+101
* Fewer float axioms.xleroy2010-05-091-4/+2
generated by cgit (git 2.34.1) at 2024-06-02 19:49:46 +0000