4 files changed, 39 insertions, 9 deletions

diff --git a/engine/evd.ml b/engine/evd.ml
index 15b4c31851..34de2f41bb 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -430,6 +430,14 @@ type evar_flags =
     restricted_evars : Evar.t Evar.Map.t;
     typeclass_evars : Evar.Set.t }
 
+type side_effect_role =
+| Schema of inductive * string
+
+type side_effects = {
+  seff_private : Safe_typing.private_constants;
+  seff_roles : side_effect_role Cmap.t;
+}
+
 type evar_map = {
   (* Existential variables *)
   defn_evars : evar_info EvMap.t;
@@ -444,7 +452,7 @@ type evar_map = {
   metas      : clbinding Metamap.t;
   evar_flags : evar_flags;
   (** Interactive proofs *)
-  effects    : Safe_typing.private_constants;
+  effects    : side_effects;
   future_goals : Evar.t list; (** list of newly created evars, to be
                                   eventually turned into goals if not solved.*)
   principal_future_goal : Evar.t option; (** if [Some e], [e] must be
@@ -672,6 +680,11 @@ let empty_evar_flags =
     restricted_evars = Evar.Map.empty;
     typeclass_evars = Evar.Set.empty }
 
+let empty_side_effects = {
+  seff_private = Safe_typing.empty_private_constants;
+  seff_roles = Cmap.empty;
+}
+
 let empty = {
   defn_evars = EvMap.empty;
   undf_evars = EvMap.empty;
@@ -680,7 +693,7 @@ let empty = {
   last_mods  = Evar.Set.empty;
   evar_flags = empty_evar_flags;
   metas      = Metamap.empty;
-  effects    = Safe_typing.empty_private_constants;
+  effects    = empty_side_effects;
   evar_names = EvNames.empty; (* id<->key for undefined evars *)
   future_goals = [];
   principal_future_goal = None;
@@ -1011,12 +1024,17 @@ exception UniversesDiffer = UState.UniversesDiffer
 (**********************************************************)
 (* Side effects *)
 
+let concat_side_effects eff eff' = {
+  seff_private = Safe_typing.concat_private eff.seff_private eff'.seff_private;
+  seff_roles = Cmap.fold Cmap.add eff.seff_roles eff'.seff_roles;
+}
+
 let emit_side_effects eff evd =
-  { evd with effects = Safe_typing.concat_private eff evd.effects;
-	     universes = UState.emit_side_effects eff evd.universes }
+  let effects = concat_side_effects eff evd.effects in
+  { evd with effects; universes = UState.emit_side_effects eff.seff_private evd.universes }
 
 let drop_side_effects evd =
-  { evd with effects = Safe_typing.empty_private_constants; }
+  { evd with effects = empty_side_effects; }
 
 let eval_side_effects evd = evd.effects
 
diff --git a/engine/evd.mli b/engine/evd.mli
index 587a1de044..5478431e14 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -307,10 +307,22 @@ 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_effect_role =
+| Schema of inductive * string
+
+type side_effects = {
+  seff_private : Safe_typing.private_constants;
+  seff_roles : 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
diff --git a/engine/proofview.mli b/engine/proofview.mli
index 60697c1611..22e67357cd 100644
--- a/engine/proofview.mli
+++ b/engine/proofview.mli
@@ -381,7 +381,7 @@ val tclENV : Environ.env tactic
 (** {7 Put-like primitives} *)
 
 (** [tclEFFECTS eff] add the effects [eff] to the current state. *)
-val tclEFFECTS : Safe_typing.private_constants -> unit tactic
+val tclEFFECTS : Evd.side_effects -> unit tactic
 
 (** [mark_as_unsafe] declares the current tactic is unsafe. *)
 val mark_as_unsafe : unit tactic
diff --git a/engine/uState.mli b/engine/uState.mli
index 3df7f9e8e9..a34d4db8a6 100644
--- a/engine/uState.mli
+++ b/engine/uState.mli
@@ -100,7 +100,7 @@ val restrict_universe_context : ContextSet.t -> LSet.t -> ContextSet.t
    universes are preserved. *)
 val restrict : t -> Univ.LSet.t -> t
 
-val demote_seff_univs : Safe_typing.private_constants Entries.definition_entry -> t -> t
+val demote_seff_univs : 'a Entries.definition_entry -> t -> t
 
 type rigid = 
   | UnivRigid