diff options
| author | Pierre-Marie Pédrot | 2016-10-06 11:17:24 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-10-06 11:27:24 +0200 |
| commit | bcecccc6973ab15bf99223764268808b89281964 (patch) | |
| tree | 27f4eed9e608fdea5c72c298d9b962586ac937d1 /kernel | |
| parent | 5892f94fd5ca3a269e51eec26c3ff8f616ce02bd (diff) | |
Removing a slow access to a named environment.
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/csymtable.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml index 6f1ace25a6..c27cb04870 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.env_named_ctx |> lookup id |> get_value |> fill_fv_cache nv id val_of_named idfun + env |> Pre_env.lookup_named id |> get_value |> fill_fv_cache nv id val_of_named idfun | Some (v, _) -> v end | FVrel i -> |