diff options
| author | Pierre-Marie Pédrot | 2016-07-08 18:06:30 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-07-08 18:14:40 +0200 |
| commit | cb2b5cc48d54ada8a2899d311253fcb12a81fd14 (patch) | |
| tree | 8d7b726ef562c42a587b06f5ff76c1d4cec21dc6 /kernel/nativelib.ml | |
| parent | 1a4a6f8947afaceb1f7a7f63d31e4d9a7d585db2 (diff) | |
Remove spurious warnings about projections when requiring modules.
Diffstat (limited to 'kernel/nativelib.ml')
0 files changed, 0 insertions, 0 deletions