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
*
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
*
Fewer float axioms.
xleroy
2010-05-09
1
-4
/
+2
*
Suppressed axioms Float.eq_zero_{true,false}, since the latter is
xleroy
2010-05-09
1
-3
/
+0
*
Revised encoding/decoding of floats
xleroy
2010-05-09
1
-0
/
+18
*
Adapted to work with Coq 8.2-1
v1.4.1
xleroy
2009-06-05
1
-1
/
+1
*
Introduction de l'operation intuoffloat (float -> unsigned int). Pas encore ...
xleroy
2008-05-30
1
-0
/
+1
*
Ajout license, README, copyright notices
xleroy
2008-01-27
1
-0
/
+15
*
Petites adaptations pour Coq 8.1gamma
xleroy
2006-11-11
1
-1
/
+1
*
Fusion de la branche "traces":
xleroy
2006-09-04
1
-1
/
+0
*
Initial import of compcert
xleroy
2006-02-09
1
-0
/
+55