Merge PR #10249: More precise type for export and inlining of private constants

Reviewed-by: gares
Ack-by: maximedenes

1 files changed, 6 insertions, 7 deletions

diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 52e15f466f..7333114eae 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -142,12 +142,11 @@ let build_by_tactic ?(side_eff=true) env sigma ?(poly=false) typ tac =
   let gk = Global, poly, Proof Theorem in
   let ce, status, univs =
     build_constant_by_tactic id sigma sign ~goal_kind:gk typ tac 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 ce.const_entry_body
-        (fun (pt, _) -> pt, ()) } in
-  let (cb, ctx), () = Future.force ce.const_entry_body in
+  let body = Future.force ce.const_entry_body in
+  let (cb, ctx) =
+    if side_eff then Safe_typing.inline_private_constants env body
+    else fst body
+  in
   let univs = UState.merge ~sideff:side_eff ~extend:true Evd.univ_rigid univs ctx in
   cb, status, univs
 
@@ -197,5 +196,5 @@ 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 ans = Safe_typing.inline_private_constants_in_constr env ans neff in
+  let (ans, _) = Safe_typing.inline_private_constants env ((ans, Univ.ContextSet.empty), neff) in
   ans, sigma