diff options
| author | Hugo Herbelin | 2017-10-31 12:40:56 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2017-11-02 11:19:07 +0100 |
| commit | 351273dcebb47b66a4e5a1952f3009c5214e03ec (patch) | |
| tree | 49ba3300a10640a37957c021dddd38c45cec34ba /interp/stdarg.ml | |
| parent | fb57fefa5f46ba8ad7be98cff81354389d87d402 (diff) | |
Naming the type of Dyn.Map for future reuse.
Diffstat (limited to 'interp/stdarg.ml')
0 files changed, 0 insertions, 0 deletions