diff options
| author | Pierre-Marie Pédrot | 2016-08-21 21:43:16 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-09-09 12:03:25 +0200 |
| commit | e046e9b7e35cbe2d419099907cdcc0909b59d52c (patch) | |
| tree | a2dda9ed30581cf917aa82b7453c1cd6050bfd0a /kernel/pre_env.mli | |
| parent | 27c93465dcf0d5233c1195d1649f5e699ed54a90 (diff) | |
Tentative fast-access named env
Diffstat (limited to 'kernel/pre_env.mli')
| -rw-r--r-- | kernel/pre_env.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/kernel/pre_env.mli b/kernel/pre_env.mli index 928a8009ec..f916c399f3 100644 --- a/kernel/pre_env.mli +++ b/kernel/pre_env.mli @@ -45,6 +45,7 @@ type named_vals = (Id.t * lazy_val) list type named_context_val = private { env_named_ctx : Context.Named.t; env_named_val : named_vals; + env_named_map : (Context.Named.Declaration.t * lazy_val) Id.Map.t; } type env = { |