diff options
| author | Pierre-Marie Pédrot | 2020-08-24 16:47:04 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-09-18 11:43:45 +0200 |
| commit | 41b407395ba6f2ce2db5dd9365c9cbcb04a4e7c0 (patch) | |
| tree | 68a46daa99ee1fa33538b94d1fa2e43c04ac2c66 /kernel/vmbytecodes.ml | |
| parent | a00a51f312720d1cfbc138664f6ea50b2d6fb3c6 (diff) | |
Clean up a bit the implemenation of dnets.
We use higher-level combinators instead of composition of low-level ones.
Diffstat (limited to 'kernel/vmbytecodes.ml')
0 files changed, 0 insertions, 0 deletions