aboutsummaryrefslogtreecommitdiff
path: root/plugins/extraction/miniml.ml
AgeCommit message (Expand)Author
2020-07-06Primitive persistent arraysMaxime Dénès
2020-03-18Update headers in the whole code base.Théo Zimmermann
2019-11-01Add extraction for primitive floatsErik Martin-Dorel
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2019-02-04Primitive integersMaxime Dénès
2018-05-04[api] Rename `global_reference` to `GlobRef.t` to follow kernel style.Emilio Jesus Gallego Arias
2018-03-10[ssreflect] Fix module scoping problems due to packing and mli files.Emilio Jesus Gallego Arias