diff options
| author | Matej Kosik | 2016-02-15 11:55:43 +0100 |
|---|---|---|
| committer | Matej Kosik | 2016-02-15 16:39:27 +0100 |
| commit | 4f041384cb27f0d24fa14b272884b4b7f69cacbe (patch) | |
| tree | 77ec4088715057e5656f0ef04bcf61395658f939 /kernel/csymtable.ml | |
| parent | 5dfb5d5e48c86dabd17ee2167c6fd5304c788474 (diff) | |
CLEANUP: Simplifying the changes done in "kernel/*"
...
...
...
...
...
...
...
...
...
...
...
...
...
...
Diffstat (limited to 'kernel/csymtable.ml')
| -rw-r--r-- | kernel/csymtable.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml index cfbb89f06c..9d58f66154 100644 --- a/kernel/csymtable.ml +++ b/kernel/csymtable.ml @@ -190,8 +190,8 @@ and slot_for_fv env fv = begin match force_lazy_val nv with | None -> let open Context.Named in - let open Context.Named.Declaration in - fill_fv_cache nv id val_of_named idfun (lookup id env.env_named_context |> get_value) + 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 -> @@ -199,8 +199,8 @@ and slot_for_fv env fv = begin match force_lazy_val rv with | None -> let open Context.Rel in - let open Context.Rel.Declaration in - fill_fv_cache rv i val_of_rel env_of_rel (lookup i env.env_rel_context |> get_value) + 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 -> |