diff options
| author | Gaëtan Gilbert | 2019-10-29 13:11:17 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-11-01 15:49:23 +0100 |
| commit | c0f7d897fc6d831de44211f75945f51603a0c6ed (patch) | |
| tree | d7dd4cd994661d8cd9f07a914f41694d0c5e1365 /kernel/nativelambda.ml | |
| parent | 78d4fb3dade71e55288a316bb04d567409982433 (diff) | |
minor cleanup of anonymous functions
Diffstat (limited to 'kernel/nativelambda.ml')
0 files changed, 0 insertions, 0 deletions