aboutsummaryrefslogtreecommitdiff
path: root/kernel/primred.ml
AgeCommit message (Expand)Author
2020-07-21Turn various anomalies into regular errors in primitive declaration pathGaëtan Gilbert
2020-07-06Primitive persistent arraysMaxime Dénès
2019-11-01Add "==", "<", "<=" in PrimFloat.vErik Martin-Dorel
2019-11-01Add next_{up,down} primitive float functionsPierre Roux
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-03-11Remove unused Retroknowledge.Register_inlineGaëtan Gilbert
2019-02-04Primitive integersMaxime Dénès