diff options
| author | Maxime Dénès | 2015-01-23 14:15:10 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2015-01-23 14:15:10 +0100 |
| commit | 4f632721be8b083126f49dd900a3294521879ec4 (patch) | |
| tree | b5e08036a9834f9e7331f5abbbb2da3c9a5cd72b /kernel/nativevalues.ml | |
| parent | feca7916eaaceea96be4c15f08895578b3703a1c (diff) | |
Extraction: fix #3629.
The control flow of extraction is hard to read due to exceptions. When meeting
an inlined constant extracted to custom code, they could desynchronize some
tables in charge of detecting name clashes, leading to an anomaly.
Diffstat (limited to 'kernel/nativevalues.ml')
0 files changed, 0 insertions, 0 deletions