diff options
Diffstat (limited to 'kernel/pre_env.ml')
| -rw-r--r-- | kernel/pre_env.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml index 72de2f1a6..d14a254d3 100644 --- a/kernel/pre_env.ml +++ b/kernel/pre_env.ml @@ -157,7 +157,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); |