diff options
| author | Erik Martin-Dorel | 2019-10-30 12:04:22 +0100 |
|---|---|---|
| committer | Pierre Roux | 2019-11-01 10:21:59 +0100 |
| commit | 22ee3faf16e9d9f528f4738d562892e9c4d653b5 (patch) | |
| tree | e3edeb31bf2e6930125a3007a6e39d1367b82db0 /kernel | |
| parent | bb8da1d5b5f59112d31fb98e763f4cd40a874f2c (diff) | |
Add some doc snippet in ExtrOCamlFloats.v
(as suggested by @silene)
Diffstat (limited to 'kernel')
0 files changed, 0 insertions, 0 deletions