diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2018-05-16 00:06:51 +0200 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2018-05-28 15:28:24 +0200 |
commit | 4552729b88058946055dddde1533057e25bfc5a9 (patch) | |
tree | 38c4c1440c9aa03430b63da175663f96bcf668dd /kernel/cClosure.ml | |
parent | b053d98fb17d2f46878f49d7adf4839ae632c10b (diff) |
Unify pre_env and env
We now have only two notions of environments in the kernel: env and
safe_env.
Diffstat (limited to 'kernel/cClosure.ml')
-rw-r--r-- | kernel/cClosure.ml | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml index 435cf0a79..4da5f0f38 100644 --- a/kernel/cClosure.ml +++ b/kernel/cClosure.ml @@ -265,7 +265,7 @@ type 'a infos_cache = { i_repr : 'a infos -> 'a infos_tab -> constr -> 'a; i_env : env; i_sigma : existential -> constr option; - i_rels : (Context.Rel.Declaration.t * Pre_env.lazy_val) Range.t; + i_rels : (Context.Rel.Declaration.t * lazy_val) Range.t; } and 'a infos = { @@ -314,12 +314,11 @@ let evar_value cache ev = cache.i_sigma ev let create mk_cl flgs env evars = - let open Pre_env in let cache = { i_repr = mk_cl; i_env = env; i_sigma = evars; - i_rels = (Environ.pre_env env).env_rel_context.env_rel_map; + i_rels = env.env_rel_context.env_rel_map; } in { i_flags = flgs; i_cache = cache } |