diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-12-29 02:48:45 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-12-29 02:52:05 +0100 |
| commit | b2eaecf0e748e3c286e1ef337f72cee6d3475162 (patch) | |
| tree | d0924cca01d4f2f592c06706db010c975c5e08c4 /interp/dumpglob.ml | |
| parent | 5122a39888cfc6afd2383d59465324dd67b69f4a (diff) | |
Fixing bug #4462: unshelve: Anomaly: Uncaught exception Not_found.
The rewrite tactic was causing an evar leak because of the use of the
Evd.remove primitive. This function did not modify the future goals of
the evarmap to remove the considered evar and thus maintained dangling
evars in there, causing the anomaly.
Diffstat (limited to 'interp/dumpglob.ml')
0 files changed, 0 insertions, 0 deletions