index
:
compcert
FPcomp
aarch64
conditional-move
dev/michalis
floatofintu
inl-cse-const
master
no-pervasives
CompCert fork with minor modifications for Vericert.
about
summary
refs
log
tree
commit
diff
stats
log msg
author
committer
range
path:
root
/
lib
/
Floats.v
Commit message (
Expand
)
Author
Age
Files
Lines
*
Use the LGPL instead of the GPL for dual-licensed files
Xavier Leroy
2021-05-08
1
-4
/
+5
*
Replace `omega` tactic with `lia`
Xavier Leroy
2020-12-29
1
-105
/
+105
*
Remove useless parameters in theorems int_round_odd_bits and int_round_odd_le
Xavier Leroy
2020-12-29
1
-8
/
+8
*
Support the use of already-installed MenhirLib and Flocq libraries
Xavier Leroy
2020-09-21
1
-2
/
+1
*
Import ListNotations explicitly
Xavier Leroy
2020-05-04
1
-0
/
+1
*
Revert "Do not use the list notation `[]`"
Xavier Leroy
2020-05-04
1
-8
/
+8
*
Do not use the list notation `[]`
Xavier Leroy
2020-05-04
1
-8
/
+8
*
Coq 8.10 compatibility: make explicit the "core" hint database
Xavier Leroy
2019-08-05
1
-2
/
+2
*
Another way to derive floatofintu from floatofint
Xavier Leroy
2019-07-17
1
-0
/
+41
*
Add floating-point square root and fused multiply-add
Xavier Leroy
2019-07-17
1
-3
/
+51
*
Revised specification of NaN payload behavior
Xavier Leroy
2019-07-12
1
-124
/
+104
*
Avoid relying on `Export` bug (#301)
Maxime Dénès
2019-07-04
1
-1
/
+2
*
Rename Fappli_IEEE_extra.v into IEEE754_extra.v
Xavier Leroy
2019-04-26
1
-1
/
+1
*
Move Z definitions out of Integers and into Zbits
Xavier Leroy
2019-04-26
1
-4
/
+3
*
lib/Coqlib.v: remove defns about multiplication, division, modulus
Xavier Leroy
2019-04-23
1
-2
/
+2
*
Floats.v: remove leftover Print commands
Xavier Leroy
2019-04-04
1
-5
/
+1
*
Floats.v: avoid using module Zlogarithm in the proofs
Xavier Leroy
2019-04-03
1
-10
/
+19
*
Upgrade embedded version of Flocq to 3.1.
Guillaume Melquiond
2019-03-27
1
-143
/
+163
*
Add functions "ordered" and "compare" to Float and Float32
Xavier Leroy
2018-12-20
1
-9
/
+20
*
Remove coq warnings (#28)
Bernhard Schommer
2017-09-22
1
-17
/
+17
*
Hybrid 64bit/32bit PowerPC port
Bernhard Schommer
2017-05-03
1
-0
/
+69
*
Port to Coq 8.5pl2
Xavier Leroy
2016-07-08
1
-12
/
+9
*
Updated PR by removing whitespaces. Bug 17450.
Bernhard Schommer
2015-10-20
1
-134
/
+134
*
Tighten and prove correct the underflow/overflow bounds for parsing of FP lit...
Xavier Leroy
2015-07-06
1
-96
/
+2
*
build_from_parsed: simplified code + correctness proof.
Xavier Leroy
2014-11-15
1
-15
/
+86
*
Upgrade to flocq 2.4.0
Jacques-Henri Jourdan
2014-10-07
1
-87
/
+94
*
The NaN behavior of float_of_single differs on PowerPC and on IA32/ARM.
xleroy
2014-07-28
1
-73
/
+18
*
Merge of "newspilling" branch:
xleroy
2014-07-23
1
-1466
/
+1016
*
Add Proof keyword so that documentation generation works
jjourdan
2014-07-04
1
-0
/
+2
*
floatoflong_from_words, floatoflongu_from_words : proof of PowerPc implementa...
jjourdan
2014-03-13
1
-89
/
+316
*
floatoflong_decomp, floatoflongu_decomp
jjourdan
2014-03-11
1
-0
/
+238
*
Introduce and use the platform-specific Archi module giving:
xleroy
2014-01-03
1
-7
/
+6
*
Floats.v, Nan.v: hard-wire the general shape of binop_pl, so that no axioms
xleroy
2013-09-14
1
-21
/
+119
*
Merge of Flocq version 2.2.0.
xleroy
2013-08-02
1
-105
/
+339
*
More accurate model of condition register flags for ARM and IA32.
xleroy
2013-07-13
1
-0
/
+6
*
Revised handling of int->float conversions:
xleroy
2013-07-08
1
-3
/
+81
*
Treat casts int64 -> float32 as primitive operations instead of two
xleroy
2013-07-03
1
-0
/
+18
*
Merge of the float32 branch:
xleroy
2013-05-19
1
-0
/
+28
*
Big merge of the newregalloc-int64 branch. Lots of changes in two directions:
xleroy
2013-04-20
1
-44
/
+28
*
Glasnost: making transparent a number of definitions that were opaque
xleroy
2013-03-10
1
-0
/
+1
*
Updated PowerPC port to new integers.
xleroy
2013-02-12
1
-1
/
+2
*
lib/Integers.v: revised and extended, faster implementation based on
xleroy
2013-02-10
1
-33
/
+29
*
Ported to Coq 8.4pl1. Merge of branches/coq-8.4.
xleroy
2013-01-29
1
-3
/
+9
*
Remove some useless "Require".
xleroy
2012-12-30
1
-2
/
+0
*
Flocq-based parsing of floating-point literals (Jacques-Henri Jourdan)
xleroy
2012-11-03
1
-3
/
+39
*
Changelog: updated
xleroy
2012-06-28
1
-0
/
+14
*
Use Flocq for floats
xleroy
2012-06-28
1
-52
/
+725
*
float->int conversions, continued: weaker axiomatization.
xleroy
2010-10-29
1
-22
/
+3
*
Float.intoffloat and Float.intuoffloat are now partial functions.
xleroy
2010-10-28
1
-6
/
+25
*
Merge of the reuse-temps branch:
xleroy
2010-09-02
1
-17
/
+101
[next]