From a4c8ee5ccffd2b56acf5e6719213e9799e077601 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 30 Sep 2016 12:33:31 +0200 Subject: Fast environment lookup for rels. We take advantage of the range structure to get a O(log n) retrieval of values bound to a rel in an environment. --- kernel/csymtable.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'kernel/csymtable.ml') diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml index 2ffe36fcf..712c66f11 100644 --- a/kernel/csymtable.ml +++ b/kernel/csymtable.ml @@ -198,7 +198,7 @@ and slot_for_fv env fv = let rv = Pre_env.lookup_rel_val i env in begin match force_lazy_val rv with | None -> - env.env_rel_context |> Context.Rel.lookup i |> RelDecl.get_value |> fill_fv_cache rv i val_of_rel env_of_rel + env |> Pre_env.lookup_rel 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