2 files changed, 25 insertions, 9 deletions
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 1aa8997710..84eba701ed 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -200,7 +200,8 @@ type evar_map = {
   univ_cstrs : Univ.universes;
   conv_pbs   : evar_constraint list;
   last_mods  : Evar.Set.t;
-  metas      : clbinding Metamap.t
+  metas      : clbinding Metamap.t;
+  effects    : Declareops.side_effects;
 }
 
 (*** Lifting primitive from EvarMap. ***)
@@ -361,6 +362,7 @@ let empty = {
   conv_pbs   = [];
   last_mods  = Evar.Set.empty;
   metas      = Metamap.empty;
+  effects    = Declareops.no_seff;
 }
 
 let has_undefined evd = not (EvMap.is_empty evd.undf_evars)
@@ -463,6 +465,17 @@ let collect_evars c =
   collrec Evar.Set.empty c
 
 (**********************************************************)
+(* Side effects *)
+
+let emit_side_effects eff evd =
+  { evd with effects = Declareops.union_side_effects eff evd.effects; }
+
+let drop_side_effects evd =
+  { evd with effects = Declareops.no_seff; }
+
+let eval_side_effects evd = evd.effects
+
+(**********************************************************)
 (* Sort variables *)
 
 let new_univ_variable evd =
@@ -659,15 +672,11 @@ type open_constr = evar_map * constr
   type ['a] *)
 type 'a sigma = {
   it : 'a ;
-  eff : Declareops.side_effects;
   sigma : evar_map
 }
 
 let sig_it x = x.it
-let sig_eff x = x.eff
 let sig_sig x = x.sigma
-let emit_side_effects eff x =
-  { x with eff = Declareops.union_side_effects eff x.eff }
 
 (**********************************************************)
 (* Failure explanation *)
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index a5ff11c7ed..5ef243e136 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -195,6 +195,17 @@ val evar_source : existential_key -> evar_map -> Evar_kinds.t located
 (** Convenience function. Wrapper around {!find} to recover the source of an
     evar in a given evar map. *)
 
+(** {5 Side-effects} *)
+
+val emit_side_effects : Declareops.side_effects -> evar_map -> evar_map
+(** Push a side-effect into the evar map. *)
+
+val eval_side_effects : evar_map -> Declareops.side_effects
+(** Return the effects contained in the evar map. *)
+
+val drop_side_effects : evar_map -> evar_map
+(** This should not be used. For hacking purposes. *)
+
 (** {5 Sort variables}
 
     Evar maps also keep track of the universe constraints defined at a given
@@ -212,8 +223,6 @@ val set_eq_sort : evar_map -> sorts -> sorts -> evar_map
 type 'a sigma = {
   it : 'a ;
   (** The base object. *)
-  eff : Declareops.side_effects;
-  (** Sideffects to be handled by the state machine. *)
   sigma : evar_map
   (** The added unification state. *)
 }
@@ -221,9 +230,7 @@ type 'a sigma = {
     ['a]. *)
 
 val sig_it  : 'a sigma -> 'a
-val sig_eff : 'a sigma -> Declareops.side_effects
 val sig_sig : 'a sigma -> evar_map
-val emit_side_effects : Declareops.side_effects -> 'a sigma -> 'a sigma
 
 (** {5 Meta machinery}