diff options
| author | Pierre-Marie Pédrot | 2018-07-24 14:38:52 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-07-24 14:41:26 +0200 |
| commit | cb15de5ec1a8a9092a2d44fde9f98a642b9330a6 (patch) | |
| tree | 6500d0e5fb0243e7dcc77bb452503099423ade37 /kernel/nativevalues.ml | |
| parent | 388e65b550a6dd12fa4e59b26e03a831ebd842ce (diff) | |
Add combinators to drop the bodies of local declarations.
Diffstat (limited to 'kernel/nativevalues.ml')
0 files changed, 0 insertions, 0 deletions