CLEANUP: Context.{Rel,Named}.Declaration.t

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 ->