From 03d50087900d51b1b88b9fbc96b35d6fd56cc602 Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Fri, 10 Oct 2014 11:47:21 +0200
Subject: Evd: a few comments to document the increasingly wide internal
 [evar_map] type.

---
 pretyping/evd.ml | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 0964baefff..05ab115ca6 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. ***)
-- 
cgit v1.2.3