Merge PR #10334: Remove the side-effect role from the kernel.

Reviewed-by: gares

5 files changed, 11 insertions, 10 deletions

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