aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/csymtable.ml
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/csymtable.ml')
-rw-r--r--kernel/csymtable.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml
index e195618b6..6f1ace25a 100644
--- a/kernel/csymtable.ml
+++ b/kernel/csymtable.ml
@@ -191,7 +191,7 @@ and slot_for_fv env fv =
| None ->
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
+ env.env_named_context.env_named_ctx |> lookup id |> get_value |> fill_fv_cache nv id val_of_named idfun
| Some (v, _) -> v
end
| FVrel i ->