Merge branch 'v8.5'

5 files changed, 18 insertions, 13 deletions

diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 2ab3dc67a5..86bc44a626 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -151,10 +151,14 @@ let build_by_tactic ?(side_eff=true) env ctx ?(poly=false) typ tac =
   let sign = val_of_named_context (named_context env) in
   let gk = Global, poly, Proof Theorem in
   let ce, status, univs = build_constant_by_tactic id ctx sign ~goal_kind:gk typ tac in
-  let ce = if side_eff then Term_typing.handle_entry_side_effects env ce else { ce with const_entry_body = Future.chain ~pure:true ce.const_entry_body (fun (pt, _) -> pt, Declareops.no_seff) } in
+  let ce =
+    if side_eff then Safe_typing.inline_private_constants_in_definition_entry env ce
+    else { ce with
+      const_entry_body = Future.chain ~pure:true ce.const_entry_body
+        (fun (pt, _) -> pt, Safe_typing.empty_private_constants) } in
   let (cb, ctx), se = Future.force ce.const_entry_body in
   let univs' = Evd.merge_context_set Evd.univ_rigid (Evd.from_ctx univs) ctx in
-  assert(Declareops.side_effects_is_empty se);
+  assert(Safe_typing.empty_private_constants = se);
   cb, status, Evd.evar_universe_context univs'
 
 let refine_by_tactic env sigma ty tac =
@@ -189,7 +193,7 @@ let refine_by_tactic 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 ans = Term_typing.handle_side_effects env ans neff in
+  let ans = Safe_typing.inline_private_constants_in_constr env ans neff in
   ans, sigma
 
 (**********************************************************************)
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index b1fba132d9..fc521ea432 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -69,11 +69,11 @@ val start_proof :
 val cook_this_proof :
     Proof_global.proof_object ->
   (Id.t *
-    (Entries.definition_entry * Proof_global.proof_universes * goal_kind))
+    (Safe_typing.private_constants Entries.definition_entry * Proof_global.proof_universes * goal_kind))
 
 val cook_proof : unit ->
   (Id.t *
-    (Entries.definition_entry * Proof_global.proof_universes * goal_kind))
+    (Safe_typing.private_constants Entries.definition_entry * Proof_global.proof_universes * goal_kind))
 
 (** {6 ... } *)
 (** [get_pftreestate ()] returns the current focused pending proof.
@@ -152,7 +152,7 @@ val instantiate_nth_evar_com : int -> Constrexpr.constr_expr -> unit
 val build_constant_by_tactic :
   Id.t -> Evd.evar_universe_context -> named_context_val -> ?goal_kind:goal_kind ->
   types -> unit Proofview.tactic -> 
-  Entries.definition_entry * bool * Evd.evar_universe_context
+  Safe_typing.private_constants Entries.definition_entry * bool * Evd.evar_universe_context
 
 val build_by_tactic : ?side_eff:bool -> env -> Evd.evar_universe_context -> ?poly:polymorphic ->
   types -> unit Proofview.tactic -> 
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 4af18ab2d5..e036ae3a15 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -67,7 +67,7 @@ type proof_universes = Evd.evar_universe_context
 
 type proof_object = {
   id : Names.Id.t;
-  entries : Entries.definition_entry list;
+  entries : Safe_typing.private_constants Entries.definition_entry list;
   persistence : Decl_kinds.goal_kind;
   universes: proof_universes;
   (* constraints : Univ.constraints; *)
@@ -323,13 +323,14 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now fpl =
         let open Universes in
         let body = c in
 	let typ =
-	  if not (keep_body_ucst_separate || not (Declareops.side_effects_is_empty eff)) then
+	  if not (keep_body_ucst_separate || not (Safe_typing.empty_private_constants = eff)) then
 	    nf t
 	  else t
 	in
         let used_univs_body = Universes.universes_of_constr body in
         let used_univs_typ = Universes.universes_of_constr typ in
-        if keep_body_ucst_separate || not (Declareops.side_effects_is_empty eff) then
+        if keep_body_ucst_separate ||
+           not (Safe_typing.empty_private_constants = eff) then
           let initunivs = Evd.evar_context_universe_context initial_euctx in
           let ctx = constrain_variables initunivs universes in
           (* For vi2vo compilation proofs are computed now but we need to
@@ -373,7 +374,7 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now fpl =
   { id = pid; entries = entries; persistence = strength; universes = universes },
   fun pr_ending -> Ephemeron.get terminator pr_ending
 
-type closed_proof_output = (Term.constr * Declareops.side_effects) list * Evd.evar_universe_context
+type closed_proof_output = (Term.constr * Safe_typing.private_constants) list * Evd.evar_universe_context
 
 let return_proof ?(allow_partial=false) () =
  let { pid; proof; strength = (_,poly,_) } = cur_pstate () in
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index 929bb86e89..a67481e71c 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -58,7 +58,7 @@ type lemma_possible_guards = int list list
 type proof_universes = Evd.evar_universe_context
 type proof_object = {
   id : Names.Id.t;
-  entries : Entries.definition_entry list;
+  entries : Safe_typing.private_constants Entries.definition_entry list;
   persistence : Decl_kinds.goal_kind;
   universes: proof_universes;
   (* constraints : Univ.constraints; *)
@@ -100,7 +100,7 @@ val close_proof : keep_body_ucst_separate:bool -> Future.fix_exn -> closed_proof
  * Both access the current proof state. The former is supposed to be
  * chained with a computation that completed the proof *)
 
-type closed_proof_output = (Term.constr * Declareops.side_effects) list * Evd.evar_universe_context
+type closed_proof_output = (Term.constr * Safe_typing.private_constants) list * Evd.evar_universe_context
 
 (* 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/proofview.mli b/proofs/proofview.mli
index 0b6c147f92..aafd4c5759 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -336,7 +336,7 @@ val tclENV : Environ.env tactic
 (** {7 Put-like primitives} *)
 
 (** [tclEFFECTS eff] add the effects [eff] to the current state. *)
-val tclEFFECTS : Declareops.side_effects -> unit tactic
+val tclEFFECTS : Safe_typing.private_constants -> unit tactic
 
 (** [mark_as_unsafe] declares the current tactic is unsafe. *)
 val mark_as_unsafe : unit tactic