diff options
| author |  Pierre Letouzey <pierre.letouzey@inria.fr> | 2015-11-29 01:05:06 +0100 |
|---|---|---|
| committer | Pierre Letouzey <pierre.letouzey@inria.fr> | 2015-12-12 18:51:37 +0100 |
| commit | e2915d2e615a271c90d9e8c8599a428ed15828b5 (patch) | |
| tree | da69e5d6178aff08caf52b0dd5bf57a6d1a8222d /plugins/extraction/mlutil.ml | |
| parent | 5550d920b831ec080cac236840132770bf1ba754 (diff) | |
Extraction: fix for bug #4334 (use of delta_resolver in Extract_env)
The ind_equiv field wasn't correctly set, due to some kernel names
glitches (canonical vs. user). The fix is to take into account the
delta_resolver while traversing module structures.
Diffstat (limited to 'plugins/extraction/mlutil.ml')
0 files changed, 0 insertions, 0 deletions