From a5d336774c7b5342c8d873d43c9b92bae42b43e7 Mon Sep 17 00:00:00 2001 From: Matej Kosik Date: Sat, 13 Aug 2016 18:11:22 +0200 Subject: CLEANUP: minor readability improvements mainly concerning referring to "Context.{Rel,Named}.get_{id,value,type}" functions. If multiple modules define a function with a same name, e.g.: Context.{Rel,Named}.get_type those calls were prefixed with a corresponding prefix to make sure that it is obvious which function is being called. --- kernel/csymtable.ml | 10 ++++------ 1 file changed, 4 insertions(+), 6 deletions(-) (limited to 'kernel/csymtable.ml') diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml index acd73d97d..3177b5fae 100644 --- a/kernel/csymtable.ml +++ b/kernel/csymtable.ml @@ -22,6 +22,8 @@ open Declarations open Pre_env open Cbytegen +module NamedDecl = Context.Named.Declaration +module RelDecl = Context.Rel.Declaration external tcode_of_code : emitcodes -> int -> tcode = "coq_tcode_of_code" external eval_tcode : tcode -> values array -> values = "coq_eval_tcode" @@ -189,18 +191,14 @@ 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 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 |> Context.Named.lookup id |> NamedDecl.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 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 + env.env_rel_context |> Context.Rel.lookup i |> RelDecl.get_value |> fill_fv_cache rv i val_of_rel env_of_rel | Some (v, _) -> v end | FVuniv_var idu -> -- cgit v1.2.3