diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/environ.mli | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/kernel/environ.mli b/kernel/environ.mli index 55df27a8b3..974e794c6b 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -69,7 +69,11 @@ type stratification = { type named_context_val = private { env_named_ctx : Constr.named_context; env_named_map : (Constr.named_declaration * lazy_val) Id.Map.t; + (** Identifier-indexed version of [env_named_ctx] *) env_named_var : Constr.t list; + (** List of identifiers in [env_named_ctx], in the same order, including + let-ins. This is not used in the kernel, but is critical to preserve + sharing of evar instances in the proof engine. *) } type rel_context_val = private { |