aboutsummaryrefslogtreecommitdiff
path: root/kernel/float64.ml
AgeCommit message (Expand)Author
2019-11-01Implement classify on primitive floatPierre Roux
2019-11-01Change return type of primitive float comparisonPierre Roux
2019-11-01Put axioms on ldshiftexp and frshiftexpGuillaume Bertholon
2019-11-01Add primitive floats to 'vm_compute'Guillaume Bertholon
2019-11-01Add primitive float computation in Coq kernelGuillaume Bertholon