diff options
Diffstat (limited to 'pretyping/evd.mli')
| -rw-r--r-- | pretyping/evd.mli | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/pretyping/evd.mli b/pretyping/evd.mli index f29a676c6..e67b1f81b 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 *) |