aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/safe_typing.ml
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2017-01-17 11:23:48 +0100
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2017-01-17 11:38:06 +0100
commit8d783c10d9505cbc1beb1c8e3451ea5dd567f260 (patch)
tree12bcf92f2a95bc8993be1674e26132c4c4cb9588 /kernel/safe_typing.ml
parent23ffecc39a064775724ad524bd97f30fb8e763cd (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 'kernel/safe_typing.ml')
0 files changed, 0 insertions, 0 deletions