aboutsummaryrefslogtreecommitdiff
path: root/kernel/primred.mli
AgeCommit message (Expand)Author
2019-11-01Implement classify on primitive floatPierre Roux
2019-11-01Change return type of primitive float comparisonPierre Roux
2019-11-01Add primitive float computation in Coq kernelGuillaume Bertholon
2019-02-04Primitive integersMaxime Dénès