Adding an extensible global state to evarmaps.

Evars already had their own extensible state, but adding it globally allows
to write out extensible state-passing code in e.g. plugins. The additional
data is hopefully transparently preserved by the code out there. Trespassers
ought to be prosecuted.

2 files changed, 22 insertions, 0 deletions

diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index f414d71dc..18e668d28 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -564,6 +564,7 @@ type evar_map = {
                                              name) of the evar which
                                              will be instantiated with
                                              a term containing [e]. *)
+  extras : Store.t;
 }
 
 (*** Lifting primitive from Evar.Map. ***)
@@ -745,6 +746,7 @@ let empty = {
   evar_names = (EvMap.empty,Idmap.empty); (* id<->key for undefined evars *)
   future_goals = [];
   principal_future_goal = None;
+  extras = Store.empty;
 }
 
 let from_env ?ctx e = 
@@ -1320,6 +1322,7 @@ let set_metas evd metas = {
   evar_names = evd.evar_names;
   future_goals = evd.future_goals;
   principal_future_goal = evd.principal_future_goal;
+  extras = Store.empty;
 }
 
 let meta_list evd = metamap_to_list evd.metas
@@ -1468,6 +1471,12 @@ let dependent_evar_ident ev evd =
   | (_,Evar_kinds.VarInstance id) -> id
   | _ -> anomaly (str "Not an evar resulting of a dependent binding")
 
+(**********************************************************)
+(* Extra data *)
+
+let get_extra_data evd = evd.extras
+let set_extra_data extras evd = { evd with extras }
+
 (*******************************************************************)
 
 type pending = (* before: *) evar_map * (* after: *) evar_map
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index eca6d60ad..15ce979d0 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -310,6 +310,19 @@ val add_universe_constraints : evar_map -> Universes.universe_constraints -> eva
     @raises UniversesDiffer in case a first-order unification fails.
     @raises UniverseInconsistency
 *)
+
+(** {5 Extra data}
+
+  Evar maps can contain arbitrary data, allowing to use an extensible state.
+  As evar maps are theoretically used in a strict state-passing style, such
+  additional data should be passed along transparently. Some old and bug-prone
+  code tends to drop them nonetheless, so you should keep cautious.
+
+*)
+
+val get_extra_data : evar_map -> Store.t
+val set_extra_data : Store.t -> evar_map -> evar_map
+
 (** {5 Enriching with evar maps} *)
 
 type 'a sigma = {