aboutsummaryrefslogtreecommitdiff
path: root/plugins/extraction/ExtrOCamlFloats.v
AgeCommit message (Expand)Author
2020-02-13[build] Consolidate stdlib's .v files under a single directory.Emilio Jesus Gallego Arias
2019-11-01Add some doc snippet in ExtrOCamlFloats.vErik Martin-Dorel
2019-11-01Add extraction for primitive floatsErik Martin-Dorel