diff options
| author | Emilio Jesus Gallego Arias | 2020-06-17 16:02:44 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-06-30 13:12:01 +0200 |
| commit | b0169fc220ced87d094177575c0dae76d8d87a50 (patch) | |
| tree | bf7370df0dd85436f11eeaa806693472fe8d046a /kernel/nativecode.ml | |
| parent | e260c203fa74a587bd78b2803c8ee046ff3df20a (diff) | |
[declaremods] Remove abstraction of imperative module operations
Now that `Printmods` is above `Declaremods`, we don't need to pass the
extra `mod_ops` argument.
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions