Remove the side-effect role from the kernel.

We move the role data into the evarmap instead.

1 files changed, 11 insertions, 2 deletions

diff --git a/engine/evd.mli b/engine/evd.mli
index 587a1de044..46b69de232 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -307,10 +307,19 @@ val dependent_evar_ident : Evar.t -> evar_map -> Id.t
 
 (** {5 Side-effects} *)
 
-val emit_side_effects : Safe_typing.private_constants -> evar_map -> evar_map
+type side_effects = {
+  seff_private : Safe_typing.private_constants;
+  seff_roles : Entries.side_effect_role Cmap.t;
+}
+
+val empty_side_effects : side_effects
+
+val concat_side_effects : side_effects -> side_effects -> side_effects
+
+val emit_side_effects : side_effects -> evar_map -> evar_map
 (** Push a side-effect into the evar map. *)
 
-val eval_side_effects : evar_map -> Safe_typing.private_constants
+val eval_side_effects : evar_map -> side_effects
 (** Return the effects contained in the evar map. *)
 
 val drop_side_effects : evar_map -> evar_map