From 207ec95b8bda34e4c905e07a1ec6462c5fdefdb0 Mon Sep 17 00:00:00 2001 From: Matej Kosik Date: Thu, 2 Feb 2017 14:35:51 +0100 Subject: simplifying "Environ.push_named" function --- kernel/pre_env.ml | 14 +------------- 1 file changed, 1 insertion(+), 13 deletions(-) (limited to 'kernel') 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) -- cgit v1.2.3