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.

1 files changed, 2 insertions, 1 deletions

diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml
index 7be8606ef4..f211583e06 100644
--- a/kernel/pre_env.ml
+++ b/kernel/pre_env.ml
@@ -156,7 +156,8 @@ let map_named_val f ctxt =
     (accu, d')
   in
   let map, ctx = List.fold_map fold ctxt.env_named_map ctxt.env_named_ctx in
-  { env_named_ctx = ctx; env_named_map = map }
+  if map == ctxt.env_named_map then ctxt
+  else { env_named_ctx = ctx; env_named_map = map }
 
 let push_named d env =
 (*  if not (env.env_rel_context = []) then raise (ASSERT env.env_rel_context);