diff options
| author | ppedrot | 2013-11-13 19:18:15 +0000 |
|---|---|---|
| committer | ppedrot | 2013-11-13 19:18:15 +0000 |
| commit | 8d6ab692ded32f861bef6c4f69cc91e19d98ccb4 (patch) | |
| tree | 84eb41c6bb56bb6c6e274d9126c9c9032003d21f /kernel/pre_env.mli | |
| parent | 2fff9290c2da7e815606673bd532a8755fe66dee (diff) | |
Fast lookup_named in environments, based on maps instead of lists.
This was quite a severe performance bottleneck.
Ideally, this data structure should be put into contexts, but the relevant
type is transparent... For now, we stick to this inelegant workaround.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17086 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/pre_env.mli')
| -rw-r--r-- | kernel/pre_env.mli | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/kernel/pre_env.mli b/kernel/pre_env.mli index f634719f9a..00939c300f 100644 --- a/kernel/pre_env.mli +++ b/kernel/pre_env.mli @@ -41,6 +41,7 @@ type named_vals = (Id.t * lazy_val) list type env = { env_globals : globals; env_named_context : named_context; + env_named_context_map : named_declaration Id.Map.t; env_named_vals : named_vals; env_rel_context : rel_context; env_rel_val : lazy_val list; @@ -49,7 +50,7 @@ type env = { env_conv_oracle : Conv_oracle.oracle; retroknowledge : Retroknowledge.retroknowledge } -type named_context_val = named_context * named_vals +type named_context_val = named_context * named_declaration Id.Map.t * named_vals val empty_named_context_val : named_context_val |