diff options
| author | Maxime Dénès | 2016-09-21 10:48:20 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2016-09-21 10:48:20 +0200 |
| commit | 530287b4cd26b10457cad95dd6b41592e21ef440 (patch) | |
| tree | 7ef7b97e2c41fc2af2ebe3b82ee312d82dfcab77 /kernel/nativecode.ml | |
| parent | 97abe11a5ea271dcde5bd0aedd69056be22220eb (diff) | |
Fix description of change in intro semantics.
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions