aboutsummaryrefslogtreecommitdiff
path: root/kernel/primred.ml
AgeCommit message (Expand)Author
2021-02-26Signed primitive integersAna
2020-10-21Introduce an Ind module in the Names API.Pierre-Marie Pédrot
2020-10-21Deprecate the non-qualified equality functions on kerpairs.Pierre-Marie Pédrot
2020-10-08Remove occurrences of Parray.reroot.Guillaume Melquiond
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