diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-05-29 15:58:21 +0200 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-05-29 16:12:50 +0200 |
commit | 35fb7ad402fee1e3e247ccf37438d3a7a5230629 (patch) | |
tree | 2280a11230b0e51787960eeeb2a36d96c63727c9 /lib/serialize.mli | |
parent | 34ba7e0d17c76c42a8ece4d195d280f7722f3bae (diff) |
Fix bug #4746: Anomaly: Evar ?X10 was not declared.
Some dubious evarmap manipulation is going on in destruct because of the
use of clenv primitives. Here, building a clenv was introducing new evars
that were not taken into account in the remainder of the tactic. We plug
them back using a local workaround.
Eventually, this code should be replaced by an evar-based one, but meanwhile,
we rely on what is probably a hack.
Diffstat (limited to 'lib/serialize.mli')
0 files changed, 0 insertions, 0 deletions