diff options
| author | Pierre-Marie Pédrot | 2020-08-06 12:37:22 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-08-06 12:45:02 +0200 |
| commit | 2edad4e3903ee77155f8b164c6cf6df49c897a27 (patch) | |
| tree | e91768f5cf63827ad4ac637095b84f47254d9ed4 | |
| parent | ed4159b617f49d3a024ac6e344c127d99208a0f7 (diff) | |
Add a few comments about the code.
| -rw-r--r-- | engine/evarutil.mli | 9 | ||||
| -rw-r--r-- | kernel/environ.mli | 4 |
2 files changed, 13 insertions, 0 deletions
diff --git a/engine/evarutil.mli b/engine/evarutil.mli index 8083bb86c3..a8fc9ef5e2 100644 --- a/engine/evarutil.mli +++ b/engine/evarutil.mli @@ -40,6 +40,15 @@ val new_evar : ?principal:bool -> ?hypnaming:naming_mode -> env -> evar_map -> types -> evar_map * EConstr.t +(** Low-level interface to create an evar. + @param src User-facing source for the evar + @param filter See {!Evd.Filter}, must be the same length as [named_context_val] + @param identity See {!Evd.Identity}, must be the name projection of [named_context_val] + @param naming A naming scheme for the evar + @param principal Whether the evar is the principal goal + @param named_context_val The context of the evar + @param types The type of conclusion of the evar +*) val new_pure_evar : ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> ?identity:EConstr.t list -> 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 { |