diff options
| author |  Arnaud Spiwack <arnaud@spiwack.net> | 2014-10-10 11:47:21 +0200 |
|---|---|---|
| committer | Arnaud Spiwack <arnaud@spiwack.net> | 2014-10-16 10:23:29 +0200 |
| commit | 03d50087900d51b1b88b9fbc96b35d6fd56cc602 (patch) | |
| tree | 6eca5386665ecc44dc3a84d7c413b25c2c14521e /pretyping/evd.ml | |
| parent | be66bcaa51298b302f798128fbf3215c123c57d8 (diff) | |
Evd: a few comments to document the increasingly wide internal [evar_map] type.
Diffstat (limited to 'pretyping/evd.ml')
| -rw-r--r-- | pretyping/evd.ml | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/pretyping/evd.ml b/pretyping/evd.ml index 0964baeff..05ab115ca 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -572,14 +572,19 @@ type evar_constraint = conv_pb * Environ.env * constr * constr module EvMap = Evar.Map type evar_map = { + (** Existential variables *) defn_evars : evar_info EvMap.t; undf_evars : evar_info EvMap.t; + evar_names : Id.t EvMap.t * existential_key Idmap.t; + (** Universes *) universes : evar_universe_context; + (** Conversion problems *) conv_pbs : evar_constraint list; last_mods : Evar.Set.t; + (** Metas *) metas : clbinding Metamap.t; + (** Interactive proofs *) effects : Declareops.side_effects; - evar_names : Id.t EvMap.t * existential_key Idmap.t; } (*** Lifting primitive from Evar.Map. ***) |