aboutsummaryrefslogtreecommitdiff
path: root/pretyping/keys.ml
AgeCommit message (Expand)Author
2020-10-21Rename the GlobRef comparison modules following the standard pattern.Pierre-Marie Pédrot
2020-07-06Primitive persistent arraysMaxime Dénès
2020-03-18Update headers in the whole code base.Théo Zimmermann
2019-11-01Add primitive float computation in Coq kernelGuillaume Bertholon
2019-08-18[api] Move `Keys` to pretypingEmilio Jesus Gallego Arias