diff options
| author | Arnaud Spiwack | 2014-08-05 11:34:02 +0200 |
|---|---|---|
| committer | Arnaud Spiwack | 2014-08-05 16:52:13 +0200 |
| commit | b19a845e7bbda10120a8a1f4b5cf92a057b5d10f (patch) | |
| tree | c8c221bdf2f924b806b4e70e9b6100619a0ee392 /kernel/nativecode.mli | |
| parent | e497afaccc78e92b71e60878d593273dce0036a1 (diff) | |
Fix [uconstr] name for argextend.
Diffstat (limited to 'kernel/nativecode.mli')
0 files changed, 0 insertions, 0 deletions