diff options
| author | Emilio Jesus Gallego Arias | 2019-10-17 18:03:18 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-10-24 21:12:55 +0200 |
| commit | 252aaae6a6955718609a94b7ae5ac707145d5064 (patch) | |
| tree | c8bf97a33ce6957ae56b364512a7297e872ca0d6 /kernel/nativecode.ml | |
| parent | 4c779c4fee1134c5d632885de60db73d56021df4 (diff) | |
[library] [nit] Remove unnecessary type alias.
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions