Statically ensuring that inlined entries out of the kernel have no effects.

This was an easy to prove property that I somehow overlooked.

5 files changed, 7 insertions, 10 deletions

diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 148fdca67..752fdd793 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -67,7 +67,7 @@ val mk_pure_proof : Constr.constr -> private_constants Entries.proof_output
 val inline_private_constants_in_constr :
   Environ.env -> Constr.constr -> private_constants -> Constr.constr
 val inline_private_constants_in_definition_entry :
-  Environ.env -> private_constants Entries.definition_entry -> private_constants Entries.definition_entry
+  Environ.env -> private_constants Entries.definition_entry -> unit Entries.definition_entry
 
 val universes_of_private : private_constants -> Univ.universe_context_set list
 
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 23c5b6f58..ed53df01f 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -654,7 +654,7 @@ let inline_entry_side_effects env ce = { ce with
   const_entry_body = Future.chain ~pure:true
     ce.const_entry_body (fun ((body, ctx), side_eff) ->
       let body, ctx',_ = inline_side_effects env body ctx side_eff in
-      (body, ctx'), empty_seff);
+      (body, ctx'), ());
 }
 
 let inline_side_effects env body side_eff =
diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli
index 5914c4a95..24153343e 100644
--- a/kernel/term_typing.mli
+++ b/kernel/term_typing.mli
@@ -30,7 +30,7 @@ val inline_side_effects : env -> constr -> side_effects -> constr
     redexes. *)
 
 val inline_entry_side_effects :
-  env -> side_effects definition_entry -> side_effects definition_entry
+  env -> side_effects definition_entry -> unit definition_entry
 (** Same as {!inline_side_effects} but applied to entries. Only modifies the
     {!Entries.const_entry_body} field. It is meant to get a term out of a not
     yet type checked proof. *)
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index a949c8e91..193788558 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -157,10 +157,9 @@ let build_by_tactic ?(side_eff=true) env sigma ?(poly=false) typ tac =
     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
+        (fun (pt, _) -> pt, ()) } in
+  let (cb, ctx), () = Future.force ce.const_entry_body in
   let univs' = Evd.merge_context_set Evd.univ_rigid (Evd.from_ctx univs) ctx in
-  assert(Safe_typing.empty_private_constants = se);
   cb, status, Evd.evar_universe_context univs'
 
 let refine_by_tactic env sigma ty tac =
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index 02067c190..28aeaa725 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -818,8 +818,7 @@ let solve_by_tac name evi t poly ctx =
     id ~goal_kind:(goal_kind poly) ctx evi.evar_hyps concl (Tacticals.New.tclCOMPLETE t) in
   let env = Global.env () in
   let entry = Safe_typing.inline_private_constants_in_definition_entry env entry in
-  let body, eff = Future.force entry.const_entry_body in
-  assert(Safe_typing.empty_private_constants = eff);
+  let body, () = Future.force entry.const_entry_body in
   let ctx' = Evd.merge_context_set ~sideff:true Evd.univ_rigid (Evd.from_ctx ctx') (snd body) in
   Inductiveops.control_only_guard (Global.env ()) (fst body);
   (fst body), entry.const_entry_type, Evd.evar_universe_context ctx'
@@ -836,8 +835,7 @@ let obligation_terminator name num guard hook auto pf =
       let env = Global.env () in
       let entry = Safe_typing.inline_private_constants_in_definition_entry env entry in
       let ty = entry.Entries.const_entry_type in
-      let (body, cstr), eff = Future.force entry.Entries.const_entry_body in
-      assert(Safe_typing.empty_private_constants = eff);
+      let (body, cstr), () = Future.force entry.Entries.const_entry_body in
       let sigma = Evd.from_ctx (fst uctx) in
       let sigma = Evd.merge_context_set ~sideff:true Evd.univ_rigid sigma cstr in
       Inductiveops.control_only_guard (Global.env ()) body;