diff options
| author | Emilio Jesus Gallego Arias | 2019-03-02 20:57:45 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-06-19 15:17:11 +0200 |
| commit | 041c09d0f59b420285723d000e4ea08fb2d3fb2d (patch) | |
| tree | 8e0e7c25e87c9d827ce7dfd711ca3f0181f2549c /kernel/nativecode.mli | |
| parent | d501690a7d767d4a542867c5b6a65a722fa8c4c1 (diff) | |
[Fail] Simplify `Fail` implementation.
We can now implement `Fail` in a direct style.
Diffstat (limited to 'kernel/nativecode.mli')
0 files changed, 0 insertions, 0 deletions