aboutsummaryrefslogtreecommitdiff
path: root/kernel/primred.mli
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-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