diff options
| author | Hugo Herbelin | 2014-11-18 10:18:00 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2014-11-18 10:26:21 +0100 |
| commit | 2e3ae20fe1ed3d7238286720c302bc892505caae (patch) | |
| tree | 74fbaa4ee461bb19b1a349c43c3d2d82dc9005a4 /kernel/nativecode.ml | |
| parent | 8d26a1d9a3846c6cbe92a9b2f17ffac6fd7d48f5 (diff) | |
Fixing a little bug with nested but convertible occurrences in "destruct at".
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions