diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-01-17 11:23:48 +0100 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-01-17 11:38:06 +0100 |
commit | 8d783c10d9505cbc1beb1c8e3451ea5dd567f260 (patch) | |
tree | 12bcf92f2a95bc8993be1674e26132c4c4cb9588 /lib/cObj.ml | |
parent | 23ffecc39a064775724ad524bd97f30fb8e763cd (diff) |
Mapping named_context_val preserves sharing when possible.
This was deactivated by 27c9346 and made an optimization moot in eauto. This
optimization was physically checking for equality, but as lists where rebuilt
by the mapping, this was never true. Some contribs were thus quite slower,
including persistent-union-find which was twice slower.
This 2-line patch fixes it by trying to preserve sharing as much as possible.
Note that we should still do something about eauto, because it does redo
useless work a lot whenever the environment only changes a bit, while we could
cache this computation.
Diffstat (limited to 'lib/cObj.ml')
0 files changed, 0 insertions, 0 deletions