index
:
debian-compcert
master
pristine-tar
upstream
Debian packaging for CompCert
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
lib
/
Floats.v
Commit message (
Expand
)
Author
Age
*
Glasnost: making transparent a number of definitions that were opaque
xleroy
2013-03-10
*
Updated PowerPC port to new integers.
xleroy
2013-02-12
*
lib/Integers.v: revised and extended, faster implementation based on
xleroy
2013-02-10
*
Ported to Coq 8.4pl1. Merge of branches/coq-8.4.
xleroy
2013-01-29
*
Remove some useless "Require".
xleroy
2012-12-30
*
Flocq-based parsing of floating-point literals (Jacques-Henri Jourdan)
xleroy
2012-11-03
*
Changelog: updated
xleroy
2012-06-28
*
Use Flocq for floats
xleroy
2012-06-28
*
float->int conversions, continued: weaker axiomatization.
xleroy
2010-10-29
*
Float.intoffloat and Float.intuoffloat are now partial functions.
xleroy
2010-10-28
*
Merge of the reuse-temps branch:
xleroy
2010-09-02
*
Fewer float axioms.
xleroy
2010-05-09
*
Suppressed axioms Float.eq_zero_{true,false}, since the latter is
xleroy
2010-05-09
*
Revised encoding/decoding of floats
xleroy
2010-05-09
*
Adapted to work with Coq 8.2-1
xleroy
2009-06-05
*
Introduction de l'operation intuoffloat (float -> unsigned int). Pas encore ...
xleroy
2008-05-30
*
Ajout license, README, copyright notices
xleroy
2008-01-27
*
Petites adaptations pour Coq 8.1gamma
xleroy
2006-11-11
*
Fusion de la branche "traces":
xleroy
2006-09-04
*
Initial import of compcert
xleroy
2006-02-09