diff options
| author | Maxime Dénès | 2017-04-04 10:41:18 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-04-04 10:41:18 +0200 |
| commit | ca0d97dd3b3033e7f87dd5e5ea09ab6f14fd881b (patch) | |
| tree | 7c5d8307a7617567fb347033d9a075b69ddc529a /interp/notation_ops.ml | |
| parent | 32bf31fda75918bf2910301dffa7b3137c81b236 (diff) | |
Fix bug #5435: [Eval native_compute in] raises anomaly.
Was introduced by 4f041384cb27f0d2. Unsoundness seems miraculously
avoided by a safeguard I put in nativecode.ml. But other kernel changes
in this commit should probably be reviewed carefully.
Diffstat (limited to 'interp/notation_ops.ml')
0 files changed, 0 insertions, 0 deletions