2 files changed, 11 insertions, 2 deletions
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 50d8b0c8cd..3b4aa094f9 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -683,10 +683,15 @@ type open_constr = evar_map * constr
   type ['a] *)
 type 'a sigma = {
   it : 'a ;
-  sigma : evar_map}
+  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 f29a676c6b..e67b1f81bd 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -246,10 +246,14 @@ type open_constr = evar_map * constr
   type ['a] *)
 type 'a sigma = {
   it : 'a ;
-  sigma : evar_map}
+  eff : Declareops.side_effects;
+  sigma : evar_map
+}
 
 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
 
 (*********************************************************
    Failure explanation *)