More precise type for Safe_typing export and inlining of private constants.

We get rid of the future wrappers, as all callers are immediately forcing
the result.

2 files changed, 10 insertions, 26 deletions

diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 873cc2a172..a90631c0f1 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -648,18 +648,10 @@ let inline_side_effects env body side_eff =
     let body = List.fold_right fold_arg args body in
     (body, ctx, sigs)
 
-let inline_private_constants_in_definition_entry env ce =
-  let open Entries in
-  { ce with
-  const_entry_body = Future.chain
-    ce.const_entry_body (fun ((body, ctx), side_eff) ->
-      let body, ctx',_ = inline_side_effects env body side_eff in
-      let ctx' = Univ.ContextSet.union ctx ctx' in
-      (body, ctx'), ());
-  }
-
-let inline_private_constants_in_constr env body side_eff =
-  pi1 (inline_side_effects env body side_eff)
+let inline_private_constants env ((body, ctx), side_eff) =
+  let body, ctx',_ = inline_side_effects env body side_eff in
+  let ctx' = Univ.ContextSet.union ctx ctx' in
+  (body, ctx')
 
 let is_suffix l suf = match l with
 | [] -> false
@@ -712,13 +704,7 @@ let constant_entry_of_side_effect eff =
 let export_eff eff =
   (eff.seff_constant, eff.seff_body, eff.seff_role)
 
-let export_side_effects mb env c =
-  let open Entries in
-      let body = c.const_entry_body in
-      let _, eff = Future.force body in
-      let ce = { c with
-        Entries.const_entry_body = Future.chain body
-          (fun (b_ctx, _) -> b_ctx, ()) } in
+let export_side_effects mb env (b_ctx, eff) =
       let not_exists e =
         try ignore(Environ.lookup_constant e.seff_constant env); false
         with Not_found -> true in
@@ -742,7 +728,7 @@ let export_side_effects mb env c =
       in
       let rec translate_seff sl seff acc env =
         match seff with
-        | [] -> List.rev acc, ce
+        | [] -> List.rev acc, b_ctx
         | eff :: rest ->
           if Int.equal sl 0 then
             let env, cb =
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 36ca3d8c47..770caf5406 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -49,10 +49,8 @@ val concat_private : private_constants -> private_constants -> private_constants
     [e1] must be more recent than those of [e2]. *)
 
 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 -> unit Entries.definition_entry
+val inline_private_constants :
+  Environ.env -> private_constants Entries.proof_output -> Constr.constr Univ.in_universe_context_set
 
 val push_private_constants : Environ.env -> private_constants -> Environ.env
 (** Push the constants in the environment if not already there. *)
@@ -93,8 +91,8 @@ type exported_private_constant =
   Constant.t * Entries.side_effect_role
 
 val export_private_constants : in_section:bool ->
-  private_constants Entries.definition_entry ->
-  (unit Entries.definition_entry * exported_private_constant list) safe_transformer
+  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) *)