Remove the side-effect role from the kernel.

We move the role data into the evarmap instead.

35 files changed, 162 insertions, 123 deletions

diff --git a/engine/evd.ml b/engine/evd.ml
index 15b4c31851..508ac0f65a 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -430,6 +430,11 @@ type evar_flags =
     restricted_evars : Evar.t Evar.Map.t;
     typeclass_evars : Evar.Set.t }
 
+type side_effects = {
+  seff_private : Safe_typing.private_constants;
+  seff_roles : Entries.side_effect_role Cmap.t;
+}
+
 type evar_map = {
   (* Existential variables *)
   defn_evars : evar_info EvMap.t;
@@ -444,7 +449,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 +677,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 +690,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 +1021,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..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
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
diff --git a/interp/declare.ml b/interp/declare.ml
index 7de92ded59..dce855bbbc 100644
--- a/interp/declare.ml
+++ b/interp/declare.ml
@@ -42,7 +42,7 @@ type constant_obj = {
   cst_locl : import_status;
 }
 
-type constant_declaration = Safe_typing.private_constants constant_entry * logical_kind
+type constant_declaration = Evd.side_effects constant_entry * logical_kind
 
 (* At load-time, the segment starting from the module name to the discharge *)
 (* section (if Remark or Fact) is needed to access a construction *)
@@ -145,7 +145,7 @@ let register_side_effect (c, role) =
 
 let default_univ_entry = Monomorphic_entry Univ.ContextSet.empty
 let definition_entry ?fix_exn ?(opaque=false) ?(inline=false) ?types
-    ?(univs=default_univ_entry) ?(eff=Safe_typing.empty_private_constants) body =
+    ?(univs=default_univ_entry) ?(eff=Evd.empty_side_effects) body =
   { const_entry_body = Future.from_val ?fix_exn ((body,Univ.ContextSet.empty), eff);
     const_entry_secctx = None;
     const_entry_type = types;
@@ -154,7 +154,14 @@ let definition_entry ?fix_exn ?(opaque=false) ?(inline=false) ?types
     const_entry_feedback = None;
     const_entry_inline_code = inline}
 
-let define_constant ?role ?(export_seff=false) id cd =
+let get_roles export eff =
+  let map c =
+    let role = try Cmap.find c eff.Evd.seff_roles with Not_found -> Subproof in
+    (c, role)
+  in
+  List.map map export
+
+let define_constant ~side_effect ?(export_seff=false) id cd =
   (* Logically define the constant and its subproofs, no libobject tampering *)
   let is_poly de = match de.const_entry_universes with
   | Monomorphic_entry _ -> false
@@ -168,26 +175,35 @@ let define_constant ?role ?(export_seff=false) id cd =
         not de.const_entry_opaque ||
         is_poly de ->
       (* This globally defines the side-effects in the environment. *)
-      let body, export = Global.export_private_constants ~in_section (Future.force de.const_entry_body) in
+      let body, eff = Future.force de.const_entry_body in
+      let body, export = Global.export_private_constants ~in_section (body, eff.Evd.seff_private) in
+      let export = get_roles export eff in
       let de = { de with const_entry_body = Future.from_val (body, ()) } in
       export, ConstantEntry (PureEntry, DefinitionEntry de)
-    | _ -> [], ConstantEntry (EffectEntry, cd)
+    | DefinitionEntry de ->
+      let map (body, eff) = body, eff.Evd.seff_private in
+      let body = Future.chain de.const_entry_body map in
+      let de = { de with const_entry_body = body } in
+      [], ConstantEntry (EffectEntry, DefinitionEntry de)
+    | ParameterEntry _ | PrimitiveEntry _ as cd ->
+      [], ConstantEntry (PureEntry, cd)
   in
-  let kn, eff = Global.add_constant ?role ~in_section id decl in
+  let kn, eff = Global.add_constant ~side_effect ~in_section id decl in
   kn, eff, export
 
 let declare_constant ?(internal = UserIndividualRequest) ?(local = ImportDefaultBehavior) id ?(export_seff=false) (cd, kind) =
   let () = check_exists id in
-  let kn, _eff, export = define_constant ~export_seff id cd in
+  let kn, (), export = define_constant ~side_effect:PureEntry ~export_seff id cd in
   (* Register the libobjects attached to the constants and its subproofs *)
   let () = List.iter register_side_effect export in
   let () = register_constant kn kind local in
   kn
 
 let declare_private_constant ~role ?(internal=UserIndividualRequest) ?(local = ImportDefaultBehavior) id (cd, kind) =
-  let kn, eff, export = define_constant ~role id cd in
+  let kn, eff, export = define_constant ~side_effect:EffectEntry id cd in
   let () = assert (List.is_empty export) in
   let () = register_constant kn kind local in
+  let eff = { Evd.seff_private = eff; Evd.seff_roles = Cmap.singleton kn role } in
   kn, eff
 
 let declare_definition ?(internal=UserIndividualRequest)
@@ -201,7 +217,7 @@ let declare_definition ?(internal=UserIndividualRequest)
 
 (** Declaration of section variables and local definitions *)
 type section_variable_entry =
-  | SectionLocalDef of Safe_typing.private_constants definition_entry
+  | SectionLocalDef of Evd.side_effects definition_entry
   | SectionLocalAssum of types Univ.in_universe_context_set * polymorphic * bool (** Implicit status *)
 
 type variable_declaration = DirPath.t * section_variable_entry * logical_kind
@@ -222,7 +238,9 @@ let cache_variable ((sp,_),o) =
     | SectionLocalDef (de) ->
       (* The body should already have been forced upstream because it is a
          section-local definition, but it's not enforced by typing *)
-      let ((body, uctx), eff) = Global.export_private_constants ~in_section:true (Future.force de.const_entry_body) in
+      let (body, eff) = Future.force de.const_entry_body in
+      let ((body, uctx), export) = Global.export_private_constants ~in_section:true (body, eff.Evd.seff_private) in
+      let eff = get_roles export eff in
       let () = List.iter register_side_effect eff in
       let poly, univs = match de.const_entry_universes with
       | Monomorphic_entry uctx -> false, uctx
diff --git a/interp/declare.mli b/interp/declare.mli
index 4120a82ca0..ed76f0a284 100644
--- a/interp/declare.mli
+++ b/interp/declare.mli
@@ -23,7 +23,7 @@ open Decl_kinds
 (** Declaration of local constructions (Variable/Hypothesis/Local) *)
 
 type section_variable_entry =
-  | SectionLocalDef of Safe_typing.private_constants definition_entry
+  | SectionLocalDef of Evd.side_effects definition_entry
   | SectionLocalAssum of types Univ.in_universe_context_set * polymorphic * bool (** Implicit status *)
 
 type variable_declaration = DirPath.t * section_variable_entry * logical_kind
@@ -33,7 +33,7 @@ val declare_variable : variable -> variable_declaration -> Libobject.object_name
 (** Declaration of global constructions 
    i.e. Definition/Theorem/Axiom/Parameter/... *)
 
-type constant_declaration = Safe_typing.private_constants constant_entry * logical_kind
+type constant_declaration = Evd.side_effects constant_entry * logical_kind
 
 type internal_flag =
   | UserAutomaticRequest
@@ -44,7 +44,7 @@ type internal_flag =
 val definition_entry : ?fix_exn:Future.fix_exn ->
   ?opaque:bool -> ?inline:bool -> ?types:types ->
   ?univs:Entries.universes_entry ->
-  ?eff:Safe_typing.private_constants -> constr -> Safe_typing.private_constants definition_entry
+  ?eff:Evd.side_effects -> constr -> Evd.side_effects definition_entry
 
 (** [declare_constant id cd] declares a global declaration
    (constant/parameter) with name [id] in the current section; it returns
@@ -56,7 +56,7 @@ val declare_constant :
  ?internal:internal_flag -> ?local:import_status -> Id.t -> ?export_seff:bool -> constant_declaration -> Constant.t
 
 val declare_private_constant :
-  role:side_effect_role -> ?internal:internal_flag -> ?local:import_status -> Id.t -> constant_declaration -> Constant.t * Safe_typing.private_constants
+  role:side_effect_role -> ?internal:internal_flag -> ?local:import_status -> Id.t -> constant_declaration -> Constant.t * Evd.side_effects
 
 val declare_definition : 
   ?internal:internal_flag -> ?opaque:bool -> ?kind:definition_object_kind ->
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 824400b4e3..0b0f14eee7 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -232,7 +232,6 @@ type side_effect = {
   from_env : Declarations.structure_body CEphemeron.key;
   seff_constant : Constant.t;
   seff_body : Constr.t Declarations.constant_body;
-  seff_role : Entries.side_effect_role;
 }
 
 module SideEffects :
@@ -536,8 +535,7 @@ type 'a effect_entry =
 type global_declaration =
   | ConstantEntry : 'a effect_entry * 'a Entries.constant_entry -> global_declaration
 
-type exported_private_constant = 
-  Constant.t * Entries.side_effect_role
+type exported_private_constant = Constant.t
 
 let add_constant_aux ~in_section senv (kn, cb) =
   let l = Constant.label kn in
@@ -699,7 +697,7 @@ let constant_entry_of_side_effect eff =
     const_entry_inline_code = cb.const_inline_code }
 
 let export_eff eff =
-  (eff.seff_constant, eff.seff_body, eff.seff_role)
+  (eff.seff_constant, eff.seff_body)
 
 let export_side_effects mb env (b_ctx, eff) =
       let not_exists e =
@@ -750,9 +748,9 @@ let n_univs cb = match cb.const_universes with
 
 let export_private_constants ~in_section ce senv =
   let exported, ce = export_side_effects senv.revstruct senv.env ce in
-  let map (kn, cb, _) = (kn, map_constant (fun p -> Opaqueproof.create ~univs:(n_univs cb) (Future.from_val (p, Univ.ContextSet.empty))) cb) in
+  let map (kn, cb) = (kn, map_constant (fun p -> Opaqueproof.create ~univs:(n_univs cb) (Future.from_val (p, Univ.ContextSet.empty))) cb) in
   let bodies = List.map map exported in
-  let exported = List.map (fun (kn, _, r) -> (kn, r)) exported in
+  let exported = List.map (fun (kn, _) -> kn) exported in
   let senv = List.fold_left (add_constant_aux ~in_section) senv bodies in
   (ce, exported), senv
 
@@ -762,7 +760,7 @@ let add_recipe ~in_section l r senv =
   let senv = add_constant_aux ~in_section senv (kn, cb) in
   kn, senv
 
-let add_constant ?role ~in_section l decl senv =
+let add_constant (type a) ~(side_effect : a effect_entry) ~in_section l decl senv : (Constant.t * a) * safe_environment =
   let kn = Constant.make2 senv.modpath l in
     let cb = 
       match decl with
@@ -786,9 +784,9 @@ let add_constant ?role ~in_section l decl senv =
       add_retroknowledge (Retroknowledge.Register_type(t,kn)) senv
     | _ -> senv
   in
-  let eff = match role with
-  | None -> empty_private_constants
-  | Some role ->
+  let eff : a = match side_effect with
+  | PureEntry -> ()
+  | EffectEntry ->
     let body, univs = match cb.const_body with
     | (Primitive _ | Undef _) -> assert false
     | Def c -> (Def c, cb.const_universes)
@@ -808,7 +806,6 @@ let add_constant ?role ~in_section l decl senv =
       from_env = from_env;
       seff_constant = kn;
       seff_body = cb;
-      seff_role = role;
     } in
     SideEffects.add eff empty_private_constants
   in
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 770caf5406..3e902303c3 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -87,18 +87,16 @@ type 'a effect_entry =
 type global_declaration =
   | ConstantEntry : 'a effect_entry * 'a Entries.constant_entry -> global_declaration
 
-type exported_private_constant = 
-  Constant.t * Entries.side_effect_role
+type exported_private_constant = Constant.t
 
 val export_private_constants : in_section:bool ->
   private_constants Entries.proof_output ->
   (Constr.constr Univ.in_universe_context_set * exported_private_constant list) safe_transformer
 
-(** returns the main constant plus a list of auxiliary constants (empty
-    unless one requires the side effects to be exported) *)
+(** returns the main constant plus a certificate of its validity *)
 val add_constant :
-  ?role:Entries.side_effect_role -> in_section:bool -> Label.t -> global_declaration ->
-    (Constant.t * private_constants) safe_transformer
+  side_effect:'a effect_entry -> in_section:bool -> Label.t -> global_declaration ->
+    (Constant.t * 'a) safe_transformer
 
 val add_recipe :
   in_section:bool -> Label.t -> Cooking.recipe -> Constant.t safe_transformer
diff --git a/library/global.ml b/library/global.ml
index d5ffae7716..3f30a63808 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -94,7 +94,7 @@ let make_sprop_cumulative () = globalize0 Safe_typing.make_sprop_cumulative
 let set_allow_sprop b = globalize0 (Safe_typing.set_allow_sprop b)
 let sprop_allowed () = Environ.sprop_allowed (env())
 let export_private_constants ~in_section cd = globalize (Safe_typing.export_private_constants ~in_section cd)
-let add_constant ?role ~in_section id d = globalize (Safe_typing.add_constant ?role ~in_section (i2l id) d)
+let add_constant ~side_effect ~in_section id d = globalize (Safe_typing.add_constant ~side_effect ~in_section (i2l id) d)
 let add_recipe ~in_section id d = globalize (Safe_typing.add_recipe ~in_section (i2l id) d)
 let add_mind id mie = globalize (Safe_typing.add_mind (i2l id) mie)
 let add_modtype id me inl = globalize (Safe_typing.add_modtype (i2l id) me inl)
diff --git a/library/global.mli b/library/global.mli
index eaa76c3117..c36cec3511 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -46,7 +46,7 @@ val export_private_constants : in_section:bool ->
   Constr.constr Univ.in_universe_context_set * Safe_typing.exported_private_constant list
 
 val add_constant :
-  ?role:Entries.side_effect_role -> in_section:bool -> Id.t -> Safe_typing.global_declaration -> Constant.t * Safe_typing.private_constants
+  side_effect:'a Safe_typing.effect_entry -> in_section:bool -> Id.t -> Safe_typing.global_declaration -> Constant.t * 'a
 val add_recipe : in_section:bool -> Id.t -> Cooking.recipe -> Constant.t
 val add_mind :
   Id.t -> Entries.mutual_inductive_entry -> MutInd.t
diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml
index 79d1c7520f..aad3967f6d 100644
--- a/plugins/derive/derive.ml
+++ b/plugins/derive/derive.ml
@@ -12,8 +12,8 @@ open Constr
 open Context
 open Context.Named.Declaration
 
-let map_const_entry_body (f:constr->constr) (x:Safe_typing.private_constants Entries.const_entry_body)
-    : Safe_typing.private_constants Entries.const_entry_body =
+let map_const_entry_body (f:constr->constr) (x: Evd.side_effects Entries.const_entry_body)
+    : Evd.side_effects Entries.const_entry_body =
   Future.chain x begin fun ((b,ctx),fx) ->
     (f b , ctx) , fx
   end
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index d1e540cceb..5363dc9a02 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -471,7 +471,7 @@ let get_funs_constant mp =
 exception No_graph_found
 exception Found_type of int
 
-let make_scheme evd (fas : (pconstant*Sorts.family) list) : Safe_typing.private_constants definition_entry list =
+let make_scheme evd (fas : (pconstant*Sorts.family) list) : Evd.side_effects definition_entry list =
   let env = Global.env () in
   let funs = List.map fst fas in
   let first_fun = List.hd funs in
@@ -597,7 +597,7 @@ let make_scheme evd (fas : (pconstant*Sorts.family) list) : Safe_typing.private_
 	   in
 	   {const with
 	      const_entry_body = 
-                (Future.from_val (Safe_typing.mk_pure_proof princ_body));
+                (Future.from_val ((princ_body, Univ.ContextSet.empty), Evd.empty_side_effects));
 	      const_entry_type = Some scheme_type
 	   }
       )
diff --git a/plugins/funind/functional_principles_types.mli b/plugins/funind/functional_principles_types.mli
index 97f9acdb3a..759c522820 100644
--- a/plugins/funind/functional_principles_types.mli
+++ b/plugins/funind/functional_principles_types.mli
@@ -34,7 +34,7 @@ val generate_functional_principle :
 exception No_graph_found
 
 val make_scheme :   Evd.evar_map ref ->
- (pconstant*Sorts.family) list -> Safe_typing.private_constants Entries.definition_entry list
+ (pconstant*Sorts.family) list -> Evd.side_effects Entries.definition_entry list
 
 val build_scheme : (Id.t*Libnames.qualid*Sorts.family) list ->  unit
 val build_case_scheme : (Id.t*Libnames.qualid*Sorts.family)  ->  unit
diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli
index 9670cf1fa7..4078c34331 100644
--- a/plugins/funind/indfun_common.mli
+++ b/plugins/funind/indfun_common.mli
@@ -44,7 +44,7 @@ val jmeq_refl : unit -> EConstr.constr
 
 val save
   :  Id.t
-  -> Safe_typing.private_constants Entries.definition_entry
+  -> Evd.side_effects Entries.definition_entry
   -> ?hook:Lemmas.declaration_hook
   -> UState.t
   -> Decl_kinds.goal_kind
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 5df223215d..0662354daf 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -141,10 +141,10 @@ let build_by_tactic ?(side_eff=true) env sigma ?(poly=false) typ tac =
   let gk = Global ImportDefaultBehavior, poly, Proof Theorem in
   let ce, status, univs =
     build_constant_by_tactic id sigma sign ~goal_kind:gk typ tac in
-  let body = Future.force ce.const_entry_body in
+  let body, eff = Future.force ce.const_entry_body in
   let (cb, ctx) =
-    if side_eff then Safe_typing.inline_private_constants env body
-    else fst body
+    if side_eff then Safe_typing.inline_private_constants env (body, eff.Evd.seff_private)
+    else body
   in
   let univs = UState.merge ~sideff:side_eff ~extend:true Evd.univ_rigid univs ctx in
   cb, status, univs
@@ -195,5 +195,6 @@ let refine_by_tactic ~name ~poly env sigma ty tac =
      other goals that were already present during its invocation, so that
      those goals rely on effects that are not present anymore. Hopefully,
      this hack will work in most cases. *)
+  let neff = neff.Evd.seff_private in
   let (ans, _) = Safe_typing.inline_private_constants env ((ans, Univ.ContextSet.empty), neff) in
   ans, sigma
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index 77d701b41f..63d5adfcd2 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -61,7 +61,7 @@ val use_unification_heuristics : unit -> bool
 val build_constant_by_tactic :
   Id.t -> UState.t -> named_context_val -> ?goal_kind:goal_kind ->
   EConstr.types -> unit Proofview.tactic -> 
-  Safe_typing.private_constants Entries.definition_entry * bool *
+  Evd.side_effects Entries.definition_entry * bool *
     UState.t
 
 val build_by_tactic : ?side_eff:bool -> env -> UState.t -> ?poly:polymorphic ->
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 8e1d16175f..96d90e9252 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -29,7 +29,7 @@ type lemma_possible_guards = int list list
 
 type proof_object = {
   id : Names.Id.t;
-  entries : Safe_typing.private_constants Entries.definition_entry list;
+  entries : Evd.side_effects Entries.definition_entry list;
   persistence : Decl_kinds.goal_kind;
   universes: UState.t;
 }
@@ -134,7 +134,7 @@ let get_open_goals ps =
     (List.map (fun (l1,l2) -> List.length l1 + List.length l2) stack) +
   List.length shelf
 
-type closed_proof_output = (Constr.t * Safe_typing.private_constants) list * UState.t
+type closed_proof_output = (Constr.t * Evd.side_effects) list * UState.t
 
 let private_poly_univs =
   let b = ref true in
@@ -172,7 +172,7 @@ let close_proof ~opaque ~keep_body_ucst_separate ?feedback_id ~now
         let body = c in
         let allow_deferred =
           not poly && (keep_body_ucst_separate ||
-          not (Safe_typing.empty_private_constants = eff))
+          not (Safe_typing.empty_private_constants = eff.Evd.seff_private))
         in
         let typ = if allow_deferred then t else nf t in
         let used_univs_body = Vars.universes_of_constr body in
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index fd0ad6fb50..f84ec27df7 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -35,7 +35,7 @@ type lemma_possible_guards = int list list
 
 type proof_object = {
   id : Names.Id.t;
-  entries : Safe_typing.private_constants Entries.definition_entry list;
+  entries : Evd.side_effects Entries.definition_entry list;
   persistence : Decl_kinds.goal_kind;
   universes: UState.t;
 }
@@ -80,7 +80,7 @@ val close_proof : opaque:opacity_flag -> keep_body_ucst_separate:bool -> Future.
  * Both access the current proof state. The former is supposed to be
  * chained with a computation that completed the proof *)
 
-type closed_proof_output = (Constr.t * Safe_typing.private_constants) list * UState.t
+type closed_proof_output = (Constr.t * Evd.side_effects) list * UState.t
 
 (* If allow_partial is set (default no) then an incomplete proof
  * is allowed (no error), and a warn is given if the proof is complete. *)
diff --git a/proofs/refine.ml b/proofs/refine.ml
index 8439156e65..d0e89183a8 100644
--- a/proofs/refine.ml
+++ b/proofs/refine.ml
@@ -60,7 +60,7 @@ let generic_refine ~typecheck f gl =
   let evs = Evd.save_future_goals sigma in
   (* Redo the effects in sigma in the monad's env *)
   let privates_csts = Evd.eval_side_effects sigma in
-  let env = Safe_typing.push_private_constants env privates_csts in
+  let env = Safe_typing.push_private_constants env privates_csts.Evd.seff_private in
   (* Check that the introduced evars are well-typed *)
   let fold accu ev = typecheck_evar ev env accu in
   let sigma = if typecheck then Evd.fold_future_goals fold sigma evs else sigma in
diff --git a/tactics/abstract.ml b/tactics/abstract.ml
index e91fe5067c..0547071519 100644
--- a/tactics/abstract.ml
+++ b/tactics/abstract.ml
@@ -173,8 +173,7 @@ let cache_term_by_tactic_then ~opaque ~name_op ?(goal_type=None) tac tacK =
   in
   let lem = mkConstU (cst, inst) in
   let evd = Evd.set_universe_context evd ectx in
-  let open Safe_typing in
-  let effs = concat_private eff
+  let effs = Evd.concat_side_effects eff
     Entries.(snd (Future.force const.const_entry_body)) in
   let solve =
     Proofview.tclEFFECTS effs <*>
diff --git a/tactics/elimschemes.ml b/tactics/elimschemes.ml
index 8ead050262..06449c38a8 100644
--- a/tactics/elimschemes.ml
+++ b/tactics/elimschemes.ml
@@ -51,7 +51,7 @@ let optimize_non_type_induction_scheme kind dep sort _ ind =
   else
     let sigma, pind = Evd.fresh_inductive_instance env sigma ind in
     let sigma, c = build_induction_scheme env sigma pind dep sort in
-      (c, Evd.evar_universe_context sigma), Safe_typing.empty_private_constants
+      (c, Evd.evar_universe_context sigma), Evd.empty_side_effects
 
 let build_induction_scheme_in_type dep sort ind =
   let env = Global.env () in
@@ -62,15 +62,15 @@ let build_induction_scheme_in_type dep sort ind =
 
 let rect_scheme_kind_from_type =
   declare_individual_scheme_object "_rect_nodep"
-    (fun _ x -> build_induction_scheme_in_type false InType x, Safe_typing.empty_private_constants)
+    (fun _ x -> build_induction_scheme_in_type false InType x, Evd.empty_side_effects)
 
 let rect_scheme_kind_from_prop =
   declare_individual_scheme_object "_rect" ~aux:"_rect_from_prop"
-    (fun _ x -> build_induction_scheme_in_type false InType x, Safe_typing.empty_private_constants)
+    (fun _ x -> build_induction_scheme_in_type false InType x, Evd.empty_side_effects)
 
 let rect_dep_scheme_kind_from_type =
   declare_individual_scheme_object "_rect" ~aux:"_rect_from_type"
-    (fun _ x -> build_induction_scheme_in_type true InType x, Safe_typing.empty_private_constants)
+    (fun _ x -> build_induction_scheme_in_type true InType x, Evd.empty_side_effects)
 
 let rec_scheme_kind_from_type =
   declare_individual_scheme_object "_rec_nodep" ~aux:"_rec_nodep_from_type"
@@ -90,7 +90,7 @@ let ind_scheme_kind_from_type =
 
 let sind_scheme_kind_from_type =
   declare_individual_scheme_object "_sind_nodep"
-  (fun _ x -> build_induction_scheme_in_type false InSProp x, Safe_typing.empty_private_constants)
+  (fun _ x -> build_induction_scheme_in_type false InSProp x, Evd.empty_side_effects)
 
 let ind_dep_scheme_kind_from_type =
   declare_individual_scheme_object "_ind" ~aux:"_ind_from_type"
@@ -98,7 +98,7 @@ let ind_dep_scheme_kind_from_type =
 
 let sind_dep_scheme_kind_from_type =
   declare_individual_scheme_object "_sind" ~aux:"_sind_from_type"
-  (fun _ x -> build_induction_scheme_in_type true InSProp x, Safe_typing.empty_private_constants)
+  (fun _ x -> build_induction_scheme_in_type true InSProp x, Evd.empty_side_effects)
 
 let ind_scheme_kind_from_prop =
   declare_individual_scheme_object "_ind" ~aux:"_ind_from_prop"
@@ -106,7 +106,7 @@ let ind_scheme_kind_from_prop =
 
 let sind_scheme_kind_from_prop =
   declare_individual_scheme_object "_sind" ~aux:"_sind_from_prop"
-  (fun _ x -> build_induction_scheme_in_type false InSProp x, Safe_typing.empty_private_constants)
+  (fun _ x -> build_induction_scheme_in_type false InSProp x, Evd.empty_side_effects)
 
 let nondep_elim_scheme from_kind to_kind =
   match from_kind, to_kind with
@@ -130,24 +130,24 @@ let build_case_analysis_scheme_in_type dep sort ind =
 
 let case_scheme_kind_from_type =
   declare_individual_scheme_object "_case_nodep"
-  (fun _ x -> build_case_analysis_scheme_in_type false InType x, Safe_typing.empty_private_constants)
+  (fun _ x -> build_case_analysis_scheme_in_type false InType x, Evd.empty_side_effects)
 
 let case_scheme_kind_from_prop =
   declare_individual_scheme_object "_case" ~aux:"_case_from_prop"
-  (fun _ x -> build_case_analysis_scheme_in_type false InType x, Safe_typing.empty_private_constants)
+  (fun _ x -> build_case_analysis_scheme_in_type false InType x, Evd.empty_side_effects)
 
 let case_dep_scheme_kind_from_type =
   declare_individual_scheme_object "_case" ~aux:"_case_from_type"
-  (fun _ x -> build_case_analysis_scheme_in_type true InType x, Safe_typing.empty_private_constants)
+  (fun _ x -> build_case_analysis_scheme_in_type true InType x, Evd.empty_side_effects)
 
 let case_dep_scheme_kind_from_type_in_prop =
   declare_individual_scheme_object "_casep_dep"
-  (fun _ x -> build_case_analysis_scheme_in_type true InProp x, Safe_typing.empty_private_constants)
+  (fun _ x -> build_case_analysis_scheme_in_type true InProp x, Evd.empty_side_effects)
 
 let case_dep_scheme_kind_from_prop =
   declare_individual_scheme_object "_case_dep"
-  (fun _ x -> build_case_analysis_scheme_in_type true InType x, Safe_typing.empty_private_constants)
+  (fun _ x -> build_case_analysis_scheme_in_type true InType x, Evd.empty_side_effects)
 
 let case_dep_scheme_kind_from_prop_in_prop =
   declare_individual_scheme_object "_casep"
-  (fun _ x -> build_case_analysis_scheme_in_type true InProp x, Safe_typing.empty_private_constants)
+  (fun _ x -> build_case_analysis_scheme_in_type true InProp x, Evd.empty_side_effects)
diff --git a/tactics/elimschemes.mli b/tactics/elimschemes.mli
index f60e6c137a..2b8a053cc0 100644
--- a/tactics/elimschemes.mli
+++ b/tactics/elimschemes.mli
@@ -18,7 +18,7 @@ val optimize_non_type_induction_scheme :
   Sorts.family ->
   'b ->
   Names.inductive ->
-  (Constr.constr * UState.t) * Safe_typing.private_constants
+  (Constr.constr * UState.t) * Evd.side_effects
 
 val rect_scheme_kind_from_prop : individual scheme_kind
 val ind_scheme_kind_from_prop : individual scheme_kind
diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml
index 3fdd97616f..d66ae9cb24 100644
--- a/tactics/eqschemes.ml
+++ b/tactics/eqschemes.ml
@@ -229,7 +229,7 @@ let sym_scheme_kind =
   declare_individual_scheme_object "_sym_internal"
   (fun _ ind ->
     let c, ctx = build_sym_scheme (Global.env() (* side-effect! *)) ind in
-      (c, ctx), Safe_typing.empty_private_constants)
+      (c, ctx), Evd.empty_side_effects)
 
 (**********************************************************************)
 (* Build the involutivity of symmetry for an inductive type           *)
@@ -455,7 +455,7 @@ let build_l2r_rew_scheme dep env ind kind =
    else
      main_body))))))
   in (c, UState.of_context_set ctx),
-      Safe_typing.concat_private eff' eff
+      Evd.concat_side_effects eff' eff
 
 (**********************************************************************)
 (* Build the left-to-right rewriting lemma for hypotheses associated  *)
@@ -708,7 +708,7 @@ let rew_l2r_dep_scheme_kind =
 (**********************************************************************)
 let rew_r2l_dep_scheme_kind =
   declare_individual_scheme_object "_rew_dep"
-  (fun _ ind -> build_r2l_rew_scheme true (Global.env()) ind InType,Safe_typing.empty_private_constants)
+  (fun _ ind -> build_r2l_rew_scheme true (Global.env()) ind InType,Evd.empty_side_effects)
 
 (**********************************************************************)
 (* Dependent rewrite from right-to-left in hypotheses                 *)
@@ -718,7 +718,7 @@ let rew_r2l_dep_scheme_kind =
 (**********************************************************************)
 let rew_r2l_forward_dep_scheme_kind =
   declare_individual_scheme_object "_rew_fwd_dep"
-  (fun _ ind -> build_r2l_forward_rew_scheme true (Global.env()) ind InType,Safe_typing.empty_private_constants)
+  (fun _ ind -> build_r2l_forward_rew_scheme true (Global.env()) ind InType,Evd.empty_side_effects)
 
 (**********************************************************************)
 (* Dependent rewrite from left-to-right in hypotheses                 *)
@@ -728,7 +728,7 @@ let rew_r2l_forward_dep_scheme_kind =
 (**********************************************************************)
 let rew_l2r_forward_dep_scheme_kind =
   declare_individual_scheme_object "_rew_fwd_r_dep"
-  (fun _ ind -> build_l2r_forward_rew_scheme true (Global.env()) ind InType,Safe_typing.empty_private_constants)
+  (fun _ ind -> build_l2r_forward_rew_scheme true (Global.env()) ind InType,Evd.empty_side_effects)
 
 (**********************************************************************)
 (* Non-dependent rewrite from either left-to-right in conclusion or   *)
@@ -742,7 +742,7 @@ let rew_l2r_forward_dep_scheme_kind =
 let rew_l2r_scheme_kind =
   declare_individual_scheme_object "_rew_r"
   (fun _ ind -> fix_r2l_forward_rew_scheme
-     (build_r2l_forward_rew_scheme false (Global.env()) ind InType), Safe_typing.empty_private_constants)
+     (build_r2l_forward_rew_scheme false (Global.env()) ind InType), Evd.empty_side_effects)
 
 (**********************************************************************)
 (* Non-dependent rewrite from either right-to-left in conclusion or   *)
@@ -752,7 +752,7 @@ let rew_l2r_scheme_kind =
 (**********************************************************************)
 let rew_r2l_scheme_kind =
   declare_individual_scheme_object "_rew"
-  (fun _ ind -> build_r2l_rew_scheme false (Global.env()) ind InType, Safe_typing.empty_private_constants)
+  (fun _ ind -> build_r2l_rew_scheme false (Global.env()) ind InType, Evd.empty_side_effects)
 
 (* End of rewriting schemes *)
 
@@ -836,4 +836,4 @@ let congr_scheme_kind = declare_individual_scheme_object "_congr"
   (fun _ ind ->
      (* May fail if equality is not defined *)
    build_congr (Global.env()) (get_coq_eq Univ.ContextSet.empty) ind,
-   Safe_typing.empty_private_constants)
+   Evd.empty_side_effects)
diff --git a/tactics/eqschemes.mli b/tactics/eqschemes.mli
index 4749aebd96..c15fa146d4 100644
--- a/tactics/eqschemes.mli
+++ b/tactics/eqschemes.mli
@@ -27,7 +27,7 @@ val rew_r2l_scheme_kind : individual scheme_kind
 val build_r2l_rew_scheme : bool -> env -> inductive -> Sorts.family -> 
   constr Evd.in_evar_universe_context
 val build_l2r_rew_scheme : bool -> env -> inductive -> Sorts.family -> 
-  constr Evd.in_evar_universe_context * Safe_typing.private_constants
+  constr Evd.in_evar_universe_context * Evd.side_effects
 val build_r2l_forward_rew_scheme :
   bool -> env -> inductive -> Sorts.family -> constr Evd.in_evar_universe_context
 val build_l2r_forward_rew_scheme :
@@ -39,7 +39,7 @@ val build_sym_scheme : env -> inductive -> constr Evd.in_evar_universe_context
 val sym_scheme_kind : individual scheme_kind
 
 val build_sym_involutive_scheme : env -> inductive -> 
-  constr Evd.in_evar_universe_context * Safe_typing.private_constants
+  constr Evd.in_evar_universe_context * Evd.side_effects
 val sym_involutive_scheme_kind : individual scheme_kind
 
 (** Builds a congruence scheme for an equality type *)
diff --git a/tactics/ind_tables.ml b/tactics/ind_tables.ml
index b9485b8823..eaff889dbf 100644
--- a/tactics/ind_tables.ml
+++ b/tactics/ind_tables.ml
@@ -31,9 +31,9 @@ open Pp
 (* Registering schemes in the environment *)
 
 type mutual_scheme_object_function =
-  internal_flag -> MutInd.t -> constr array Evd.in_evar_universe_context * Safe_typing.private_constants
+  internal_flag -> MutInd.t -> constr array Evd.in_evar_universe_context * Evd.side_effects
 type individual_scheme_object_function =
-  internal_flag -> inductive -> constr Evd.in_evar_universe_context * Safe_typing.private_constants
+  internal_flag -> inductive -> constr Evd.in_evar_universe_context * Evd.side_effects
 
 type 'a scheme_kind = string
 
@@ -124,7 +124,7 @@ let define internal role id c poly univs =
   let entry = {
     const_entry_body =
       Future.from_val ((c,Univ.ContextSet.empty),
-                       Safe_typing.empty_private_constants);
+                       Evd.empty_side_effects);
     const_entry_secctx = None;
     const_entry_type = None;
     const_entry_universes = univs;
@@ -148,7 +148,7 @@ let define_individual_scheme_base kind suff f mode idopt (mind,i as ind) =
   let role = Entries.Schema (ind, kind) in
   let const, neff = define mode role id c (Declareops.inductive_is_polymorphic mib) ctx in
   declare_scheme kind [|ind,const|];
-  const, Safe_typing.concat_private neff eff
+  const, Evd.concat_side_effects neff eff
 
 let define_individual_scheme kind mode names (mind,i as ind) =
   match Hashtbl.find scheme_object_table kind with
@@ -165,7 +165,7 @@ let define_mutual_scheme_base kind suff f mode names mind =
   let fold i effs id cl =
     let role = Entries.Schema ((mind, i), kind)in
     let cst, neff = define mode role id cl (Declareops.inductive_is_polymorphic mib) ctx in
-    (Safe_typing.concat_private neff effs, cst)
+    (Evd.concat_side_effects neff effs, cst)
   in
   let (eff, consts) = Array.fold_left2_map_i fold eff ids cl in
   let schemes = Array.mapi (fun i cst -> ((mind,i),cst)) consts in
@@ -180,7 +180,7 @@ let define_mutual_scheme kind mode names mind =
 
 let find_scheme_on_env_too kind ind =
   let s = String.Map.find kind (Indmap.find ind !scheme_map) in
-  s, Safe_typing.empty_private_constants
+  s, Evd.empty_side_effects
 
 let find_scheme ?(mode=InternalTacticRequest) kind (mind,i as ind) =
   try find_scheme_on_env_too kind ind
diff --git a/tactics/ind_tables.mli b/tactics/ind_tables.mli
index 0eb4e47aeb..460b1f1b07 100644
--- a/tactics/ind_tables.mli
+++ b/tactics/ind_tables.mli
@@ -22,9 +22,9 @@ type individual
 type 'a scheme_kind
 
 type mutual_scheme_object_function =
-  internal_flag -> MutInd.t -> constr array Evd.in_evar_universe_context * Safe_typing.private_constants
+  internal_flag -> MutInd.t -> constr array Evd.in_evar_universe_context * Evd.side_effects
 type individual_scheme_object_function =
-  internal_flag -> inductive -> constr Evd.in_evar_universe_context * Safe_typing.private_constants
+  internal_flag -> inductive -> constr Evd.in_evar_universe_context * Evd.side_effects
 
 (** Main functions to register a scheme builder *)
 
@@ -39,13 +39,13 @@ val declare_individual_scheme_object : string -> ?aux:string ->
 
 val define_individual_scheme : individual scheme_kind -> 
   internal_flag (** internal *) ->
-  Id.t option -> inductive -> Constant.t * Safe_typing.private_constants
+  Id.t option -> inductive -> Constant.t * Evd.side_effects
 
 val define_mutual_scheme : mutual scheme_kind -> internal_flag (** internal *) ->
-  (int * Id.t) list -> MutInd.t -> Constant.t array * Safe_typing.private_constants
+  (int * Id.t) list -> MutInd.t -> Constant.t array * Evd.side_effects
 
 (** Main function to retrieve a scheme in the cache or to generate it *)
-val find_scheme : ?mode:internal_flag -> 'a scheme_kind -> inductive -> Constant.t * Safe_typing.private_constants
+val find_scheme : ?mode:internal_flag -> 'a scheme_kind -> inductive -> Constant.t * Evd.side_effects
 
 val check_scheme : 'a scheme_kind -> inductive -> bool
 
diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml
index 5aec5cac2c..2e84c3275b 100644
--- a/vernac/auto_ind_decl.ml
+++ b/vernac/auto_ind_decl.ml
@@ -195,7 +195,7 @@ let build_beq_scheme mode kn =
         let (c,a) = Reductionops.whd_betaiota_stack Evd.empty EConstr.(of_constr c) in
         let (c,a) = EConstr.Unsafe.(to_constr c, List.map to_constr a) in
         match Constr.kind c with
-        | Rel x -> mkRel (x-nlist+ndx), Safe_typing.empty_private_constants
+        | Rel x -> mkRel (x-nlist+ndx), Evd.empty_side_effects
         | Var x ->
           (* Support for working in a context with "eq_x : x -> x -> bool" *)
           let eid = Id.of_string ("eq_"^(Id.to_string x)) in
@@ -203,11 +203,11 @@ let build_beq_scheme mode kn =
             try ignore (Environ.lookup_named eid env)
             with Not_found -> raise (ParameterWithoutEquality (VarRef x))
           in
-          mkVar eid, Safe_typing.empty_private_constants
+          mkVar eid, Evd.empty_side_effects
         | Cast (x,_,_) -> aux (Term.applist (x,a))
         | App _ -> assert false
         | Ind ((kn',i as ind'),u) (*FIXME: universes *) -> 
-            if MutInd.equal kn kn' then mkRel(eqA-nlist-i+nb_ind-1), Safe_typing.empty_private_constants
+            if MutInd.equal kn kn' then mkRel(eqA-nlist-i+nb_ind-1), Evd.empty_side_effects
             else begin
               try
                 let eq, eff =
@@ -216,7 +216,7 @@ let build_beq_scheme mode kn =
                 let eqa, eff =
                   let eqa, effs = List.split (List.map aux a) in
                   Array.of_list eqa,
-                  List.fold_left Safe_typing.concat_private eff (List.rev effs)
+                  List.fold_left Evd.concat_side_effects eff (List.rev effs)
                   in
                 let args =
                   Array.append
@@ -239,7 +239,7 @@ let build_beq_scheme mode kn =
                  let kneq = Constant.change_label kn eq_lbl in
                  try let _ = Environ.constant_opt_value_in env (kneq, u) in
                    Term.applist (mkConst kneq,a),
-                   Safe_typing.empty_private_constants
+                   Evd.empty_side_effects
                  with Not_found -> raise (ParameterWithoutEquality (ConstRef kn)))
         | Proj _ -> raise (EqUnknown "projection")
         | Construct _ -> raise (EqUnknown "constructor")
@@ -270,7 +270,7 @@ let build_beq_scheme mode kn =
     let constrsi = constrs (3+nparrec) in
     let n = Array.length constrsi in
     let ar = Array.make n (ff ()) in
-    let eff = ref Safe_typing.empty_private_constants in
+    let eff = ref Evd.empty_side_effects in
 	for i=0 to n-1 do
 	  let nb_cstr_args = List.length constrsi.(i).cs_args in
           let ar2 = Array.make n (ff ()) in
@@ -288,7 +288,7 @@ let build_beq_scheme mode kn =
                                           (nb_cstr_args+ndx+1)
                                           cc
                           in
-                          eff := Safe_typing.concat_private eff' !eff;
+                          eff := Evd.concat_side_effects eff' !eff;
                           Array.set eqs ndx
                               (mkApp (eqA,
                                 [|mkRel (ndx+1+nb_cstr_args);mkRel (ndx+1)|]
@@ -320,7 +320,7 @@ let build_beq_scheme mode kn =
     let names = Array.make nb_ind (make_annot Anonymous Sorts.Relevant) and
         types = Array.make nb_ind mkSet and
         cores = Array.make nb_ind mkSet in
-    let eff = ref Safe_typing.empty_private_constants in
+    let eff = ref Evd.empty_side_effects in
     let u = Univ.Instance.empty in
     for i=0 to (nb_ind-1) do
         names.(i) <- make_annot (Name (Id.of_string (rec_name i))) Sorts.Relevant;
@@ -328,7 +328,7 @@ let build_beq_scheme mode kn =
                      (mkArrow (mkFullInd ((kn,i),u) 1) Sorts.Relevant (bb ()));
         let c, eff' = make_one_eq i in
         cores.(i) <- c;
-        eff := Safe_typing.concat_private eff' !eff
+        eff := Evd.concat_side_effects eff' !eff
     done;
       (Array.init nb_ind (fun i ->
       let kelim = Inductive.elim_sort (mib,mib.mind_packets.(i)) in
@@ -938,7 +938,7 @@ let compute_dec_tact ind lnamesparrec nparrec =
     Not_found ->
       Tacticals.New.tclZEROMSG (str "Error during the decidability part, leibniz to boolean equality is required.")
   end >>= fun (lbI,eff'') ->
-  let eff = (Safe_typing.concat_private eff'' (Safe_typing.concat_private eff' eff)) in
+  let eff = (Evd.concat_side_effects eff'' (Evd.concat_side_effects eff' eff)) in
   Tacticals.New.tclTHENLIST [
         Proofview.tclEFFECTS eff;
         intros_using fresh_first_intros;
@@ -1005,7 +1005,7 @@ let make_eq_decidability mode mind =
     (EConstr.of_constr (compute_dec_goal (ind,u) lnamesparrec nparrec))
     (compute_dec_tact ind lnamesparrec nparrec)
   in
-  ([|ans|], ctx), Safe_typing.empty_private_constants
+  ([|ans|], ctx), Evd.empty_side_effects
 
 let eq_dec_scheme_kind =
   declare_mutual_scheme_object "_eq_dec" make_eq_decidability
diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml
index 4cae4b8a74..1046e354a7 100644
--- a/vernac/comDefinition.ml
+++ b/vernac/comDefinition.ml
@@ -86,7 +86,7 @@ let do_definition ~program_mode ?hook ident k univdecl bl red_option c ctypopt =
   if program_mode then
     let env = Global.env () in
     let (c,ctx), sideff = Future.force ce.const_entry_body in
-    assert(Safe_typing.empty_private_constants = sideff);
+    assert(Safe_typing.empty_private_constants = sideff.Evd.seff_private);
     assert(Univ.ContextSet.is_empty ctx);
     Obligations.check_evars env evd;
     let c = EConstr.of_constr c in
diff --git a/vernac/comDefinition.mli b/vernac/comDefinition.mli
index c3575594b6..0d9df47ee8 100644
--- a/vernac/comDefinition.mli
+++ b/vernac/comDefinition.mli
@@ -41,5 +41,5 @@ val interp_definition
   -> red_expr option
   -> constr_expr
   -> constr_expr option
-  -> Safe_typing.private_constants definition_entry *
+  -> Evd.side_effects definition_entry *
      Evd.evar_map * UState.universe_decl * Impargs.manual_implicits
diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml
index 3a25cb496c..6068cd90f1 100644
--- a/vernac/comFixpoint.ml
+++ b/vernac/comFixpoint.ml
@@ -286,7 +286,8 @@ let declare_fixpoint local poly ((fixnames,fixrs,fixdefs,fixtypes),pl,ctx,fiximp
   let evd = Evd.restrict_universe_context evd vars in
   let ctx = Evd.check_univ_decl ~poly evd pl in
   let pl = Evd.universe_binders evd in
-  let fixdecls = List.map Safe_typing.mk_pure_proof fixdecls in
+  let mk_pure c = (c, Univ.ContextSet.empty), Evd.empty_side_effects in
+  let fixdecls = List.map mk_pure fixdecls in
   ignore (List.map4 (DeclareDef.declare_fix (local, poly, Fixpoint) pl ctx)
             fixnames fixdecls fixtypes fiximps);
   (* Declare the recursive definitions *)
@@ -316,7 +317,8 @@ let declare_cofixpoint local poly ((fixnames,fixrs,fixdefs,fixtypes),pl,ctx,fixi
   let fixdecls = prepare_recursive_declaration fixnames fixrs fixtypes fixdefs in
   let fixdecls = List.map_i (fun i _ -> mkCoFix (i,fixdecls)) 0 fixnames in
   let vars = Vars.universes_of_constr (List.hd fixdecls) in
-  let fixdecls = List.map Safe_typing.mk_pure_proof fixdecls in
+  let mk_pure c = (c, Univ.ContextSet.empty), Evd.empty_side_effects in
+  let fixdecls = List.map mk_pure fixdecls in
   let fiximps = List.map (fun (len,imps,idx) -> imps) fiximps in
   let evd = Evd.from_ctx ctx in
   let evd = Evd.restrict_universe_context evd vars in
diff --git a/vernac/declareDef.mli b/vernac/declareDef.mli
index 2b9d9567cd..909aa41a30 100644
--- a/vernac/declareDef.mli
+++ b/vernac/declareDef.mli
@@ -15,7 +15,7 @@ val declare_definition
   : Id.t
   -> definition_kind
   -> ?hook_data:(Lemmas.declaration_hook * UState.t * (Id.t * Constr.t) list)
-  -> Safe_typing.private_constants Entries.definition_entry
+  -> Evd.side_effects Entries.definition_entry
   -> UnivNames.universe_binders
   -> Impargs.manual_implicits
   -> GlobRef.t
@@ -27,7 +27,7 @@ val declare_fix
   -> UnivNames.universe_binders
   -> Entries.universes_entry
   -> Id.t
-  -> Safe_typing.private_constants Entries.proof_output
+  -> Evd.side_effects Entries.proof_output
   -> Constr.types
   -> Impargs.manual_implicits
   -> GlobRef.t
@@ -36,7 +36,7 @@ val prepare_definition : allow_evars:bool ->
   ?opaque:bool -> ?inline:bool -> poly:bool ->
   Evd.evar_map -> UState.universe_decl ->
   types:EConstr.t option -> body:EConstr.t ->
-  Evd.evar_map * Safe_typing.private_constants Entries.definition_entry
+  Evd.evar_map * Evd.side_effects Entries.definition_entry
 
 val prepare_parameter : allow_evars:bool ->
   poly:bool -> Evd.evar_map -> UState.universe_decl -> EConstr.types ->
diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml
index de7d2fd49a..f18cf17bf9 100644
--- a/vernac/indschemes.ml
+++ b/vernac/indschemes.ml
@@ -414,7 +414,7 @@ let do_mutual_induction_scheme ?(force_mutual=false) lnamedepindsort =
   let declare decl fi lrecref =
     let decltype = Retyping.get_type_of env0 sigma (EConstr.of_constr decl) in
     let decltype = EConstr.to_constr sigma decltype in
-    let proof_output = Future.from_val ((decl,Univ.ContextSet.empty),Safe_typing.empty_private_constants) in
+    let proof_output = Future.from_val ((decl,Univ.ContextSet.empty),Evd.empty_side_effects) in
     let cst = define ~poly fi UserIndividualRequest sigma proof_output (Some decltype) in
     ConstRef cst :: lrecref
   in
@@ -536,7 +536,7 @@ let do_combined_scheme name schemes =
       schemes
   in
   let sigma,body,typ = build_combined_scheme (Global.env ()) csts in
-  let proof_output = Future.from_val ((body,Univ.ContextSet.empty),Safe_typing.empty_private_constants) in
+  let proof_output = Future.from_val ((body,Univ.ContextSet.empty),Evd.empty_side_effects) in
   (* It is possible for the constants to have different universe
      polymorphism from each other, however that is only when the user
      manually defined at least one of them (as Scheme would pick the
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 4e346a9564..a7366b2c56 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -112,7 +112,7 @@ let adjust_guardness_conditions const = function
 	  List.interval 0 (List.length ((lam_assum c))))
 	  lemma_guard (Array.to_list fixdefs) in
 *)
-              let env = Safe_typing.push_private_constants env eff in
+              let env = Safe_typing.push_private_constants env eff.Evd.seff_private in
               let indexes =
                 search_guard env
                   possible_indexes fixdecls in
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index 6c9ec95c5f..50d24c20c9 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -497,7 +497,7 @@ let compute_possible_guardness_evidences n fixbody fixtype =
       let ctx = fst (decompose_prod_n_assum m fixtype) in
 	List.map_i (fun i _ -> i) 0 ctx
 
-let mk_proof c = ((c, Univ.ContextSet.empty), Safe_typing.empty_private_constants)
+let mk_proof c = ((c, Univ.ContextSet.empty), Evd.empty_side_effects)
 
 let declare_mutual_definition l =
   let len = List.length l in
@@ -632,7 +632,7 @@ let declare_obligation prg obl body ty uctx =
 	if get_shrink_obligations () && not poly then
 	  shrink_body body ty else [], body, ty, [||]
       in
-      let body = ((body,Univ.ContextSet.empty),Safe_typing.empty_private_constants) in
+      let body = ((body,Univ.ContextSet.empty), Evd.empty_side_effects) in
       let ce =
         { const_entry_body = Future.from_val ~fix_exn:(fun x -> x) body;
           const_entry_secctx = None;
@@ -822,8 +822,8 @@ let solve_by_tac ?loc name evi t poly ctx =
       Pfedit.build_constant_by_tactic
         id ~goal_kind:(goal_kind poly) ctx evi.evar_hyps evi.evar_concl t in
     let env = Global.env () in
-    let body = Future.force entry.const_entry_body in
-    let body = Safe_typing.inline_private_constants env body in
+    let (body, eff) = Future.force entry.const_entry_body in
+    let body = Safe_typing.inline_private_constants env (body, eff.Evd.seff_private) in
     let ctx' = Evd.merge_context_set ~sideff:true Evd.univ_rigid (Evd.from_ctx ctx') (snd body) in
     Inductiveops.control_only_guard env ctx' (EConstr.of_constr (fst body));
     Some (fst body, entry.const_entry_type, Evd.evar_universe_context ctx')
@@ -848,8 +848,8 @@ let obligation_terminator ?hook name num guard auto pf =
   | Proved (opq, id, { entries=[entry]; universes=uctx } ) -> begin
     let env = Global.env () in
     let ty = entry.Entries.const_entry_type in
-    let body = Future.force entry.const_entry_body in
-    let (body, cstr) = Safe_typing.inline_private_constants env body in
+    let body, eff = Future.force entry.const_entry_body in
+    let (body, cstr) = Safe_typing.inline_private_constants env (body, eff.Evd.seff_private) in
     let sigma = Evd.from_ctx uctx in
     let sigma = Evd.merge_context_set ~sideff:true Evd.univ_rigid sigma cstr in
     Inductiveops.control_only_guard (Global.env ()) sigma (EConstr.of_constr body);
diff --git a/vernac/record.ml b/vernac/record.ml
index 6101e13edd..c777ef2c2b 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -344,7 +344,7 @@ let declare_projections indsp ctx ?(kind=StructureComponent) binder_name flags f
 	        try
 		  let entry = {
 		    const_entry_body =
-		      Future.from_val (Safe_typing.mk_pure_proof proj);
+                      Future.from_val ((proj, Univ.ContextSet.empty), Evd.empty_side_effects);
 		    const_entry_secctx = None;
 		    const_entry_type = Some projtyp;
                     const_entry_universes = ctx;