diff options
| author | ppedrot | 2013-10-29 15:30:34 +0000 |
|---|---|---|
| committer | ppedrot | 2013-10-29 15:30:34 +0000 |
| commit | 77e518644b1295708734e8721e7d8422612983dd (patch) | |
| tree | ec0d1f3686044fa1d0d42293753fbd54131e4032 /kernel | |
| parent | 27ec462f6f1de3a03612137c3165799b4e462e1b (diff) | |
Allocation-friendly version of [Pre_env.push_named].
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16947 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/pre_env.ml | 11 |
1 files changed, 8 insertions, 3 deletions
diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml index 61fb6b07bd..9a2bb73d1f 100644 --- a/kernel/pre_env.ml +++ b/kernel/pre_env.ml @@ -111,9 +111,14 @@ let push_named d env = assert (env.env_rel_context = []); *) let id,body,_ = d in let rval = ref VKnone in - { env with - env_named_context = Context.add_named_decl d env.env_named_context; - env_named_vals = (id,rval):: env.env_named_vals } + { env_globals = env.env_globals; + env_named_context = Context.add_named_decl d env.env_named_context; + env_named_vals = (id, rval) :: env.env_named_vals; + 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; + retroknowledge = env.retroknowledge; } let lookup_named_val id env = snd(List.find (fun (id',_) -> Id.equal id id') env.env_named_vals) |