aboutsummaryrefslogtreecommitdiff
path: root/plugins/extraction/miniml.ml
AgeCommit message (Expand)Author
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