diff options
author | 2017-02-02 14:35:51 +0100 | |
---|---|---|
committer | 2017-04-20 13:11:50 +0200 | |
commit | 207ec95b8bda34e4c905e07a1ec6462c5fdefdb0 (patch) | |
tree | 749f2d1cddbd0c19937b86b70694ffa02694789d | |
parent | dda06512833eea2805a8406b407494014371b2be (diff) |
simplifying "Environ.push_named" function
-rw-r--r-- | kernel/pre_env.ml | 14 |
1 files changed, 1 insertions, 13 deletions
diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml index d14a254d3..6bfba2d40 100644 --- a/kernel/pre_env.ml +++ b/kernel/pre_env.ml @@ -161,19 +161,7 @@ let map_named_val f 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); - assert (env.env_rel_context = []); *) - { env_globals = env.env_globals; - env_named_context = push_named_context_val d env.env_named_context; - env_rel_context = env.env_rel_context; - env_rel_val = env.env_rel_val; - env_nb_rel = env.env_nb_rel; - env_stratification = env.env_stratification; - env_typing_flags = env.env_typing_flags; - env_conv_oracle = env.env_conv_oracle; - retroknowledge = env.retroknowledge; - indirect_pterms = env.indirect_pterms; - } + {env with env_named_context = push_named_context_val d env.env_named_context} let lookup_named id env = fst (Id.Map.find id env.env_named_context.env_named_map) |