diff options
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 50d8b0c8c..3b4aa094f 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 *) |