aboutsummaryrefslogtreecommitdiff
path: root/kernel/csymtable.ml
diff options
context:
space:
mode:
authorMatej Kosik2016-02-15 19:11:42 +0100
committerMatej Kosik2016-02-15 19:11:42 +0100
commit97d6583a0b9a65080639fb02deba4200f6276ce6 (patch)
tree7e3407649be5fc1f9d47c891b0591ffd4e468468 /kernel/csymtable.ml
parent5180ab68819f10949cd41a2458bff877b3ec3204 (diff)
parent4f041384cb27f0d24fa14b272884b4b7f69cacbe (diff)
merging conflicts with the original "trunk__CLEANUP__Context__2" branch
Diffstat (limited to 'kernel/csymtable.ml')
-rw-r--r--kernel/csymtable.ml10
1 files changed, 6 insertions, 4 deletions
diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml
index 8f60216afa..9d58f66154 100644
--- a/kernel/csymtable.ml
+++ b/kernel/csymtable.ml
@@ -189,16 +189,18 @@ and slot_for_fv env fv =
let nv = Pre_env.lookup_named_val id env in
begin match force_lazy_val nv with
| None ->
- let _, b, _ = Context.Named.lookup id env.env_named_context in
- fill_fv_cache nv id val_of_named idfun b
+ let open Context.Named in
+ let open Declaration in
+ env.env_named_context |> lookup id |> get_value |> fill_fv_cache nv id val_of_named idfun
| Some (v, _) -> v
end
| FVrel i ->
let rv = Pre_env.lookup_rel_val i env in
begin match force_lazy_val rv with
| None ->
- let _, b, _ = Context.Rel.lookup i env.env_rel_context in
- fill_fv_cache rv i val_of_rel env_of_rel b
+ let open Context.Rel in
+ let open Declaration in
+ env.env_rel_context |> lookup i |> get_value |> fill_fv_cache rv i val_of_rel env_of_rel
| Some (v, _) -> v
end
| FVuniv_var idu ->