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.

6 files changed, 26 insertions, 43 deletions

diff --git a/interp/declare.ml b/interp/declare.ml
index 7ee7ecb5e8..b3595b2dae 100644
--- a/interp/declare.ml
+++ b/interp/declare.ml
@@ -163,7 +163,8 @@ let define_constant ?role ?(export_seff=false) id cd =
         not de.const_entry_opaque ||
         is_poly de ->
       (* This globally defines the side-effects in the environment. *)
-      let de, export = Global.export_private_constants ~in_section de in
+      let body, export = Global.export_private_constants ~in_section (Future.force de.const_entry_body) in
+      let de = { de with const_entry_body = Future.from_val (body, ()) } in
       export, ConstantEntry (PureEntry, DefinitionEntry de)
     | _ -> [], ConstantEntry (EffectEntry, cd)
   in
@@ -214,11 +215,10 @@ let cache_variable ((sp,_),o) =
       let impl = if impl then Implicit else Explicit in
         impl, true, poly, ctx
     | SectionLocalDef (de) ->
-      let (de, eff) = Global.export_private_constants ~in_section:true de in
-      let () = List.iter register_side_effect eff in
       (* The body should already have been forced upstream because it is a
          section-local definition, but it's not enforced by typing *)
-      let (body, uctx), () = Future.force de.const_entry_body in
+      let ((body, uctx), eff) = Global.export_private_constants ~in_section:true (Future.force de.const_entry_body) in
+      let () = List.iter register_side_effect eff in
       let poly, univs = match de.const_entry_universes with
       | Monomorphic_entry uctx -> false, uctx
       | Polymorphic_entry (_, uctx) -> true, Univ.ContextSet.of_context uctx
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) *)
diff --git a/library/global.mli b/library/global.mli
index aa9fc18477..eaa76c3117 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -42,8 +42,8 @@ val push_named_assum : (Id.t * Constr.types * bool) Univ.in_universe_context_set
 val push_named_def   : (Id.t * Entries.section_def_entry) -> unit
 
 val export_private_constants : in_section:bool ->
-  Safe_typing.private_constants Entries.definition_entry ->
-  unit Entries.definition_entry * Safe_typing.exported_private_constant list
+  Safe_typing.private_constants Entries.proof_output ->
+  Constr.constr Univ.in_universe_context_set * Safe_typing.exported_private_constant list
 
 val add_constant :
   ?role:Entries.side_effect_role -> in_section:bool -> Id.t -> Safe_typing.global_declaration -> Constant.t * Safe_typing.private_constants
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
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index ad175511b9..bc741a0ec7 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -820,8 +820,8 @@ let solve_by_tac ?loc name evi t poly ctx =
       Pfedit.build_constant_by_tactic
         id ~goal_kind:(goal_kind poly) ctx evi.evar_hyps evi.evar_concl t in
     let env = Global.env () in
-    let entry = Safe_typing.inline_private_constants_in_definition_entry env entry in
-    let body, () = Future.force entry.const_entry_body in
+    let body = Future.force entry.const_entry_body in
+    let body = Safe_typing.inline_private_constants env body in
     let ctx' = Evd.merge_context_set ~sideff:true Evd.univ_rigid (Evd.from_ctx ctx') (snd body) in
     Inductiveops.control_only_guard env ctx' (EConstr.of_constr (fst body));
     Some (fst body, entry.const_entry_type, Evd.evar_universe_context ctx')
@@ -844,9 +844,9 @@ let obligation_terminator ?hook name num guard auto pf =
   | Admitted _ -> apply_terminator term pf
   | Proved (opq, id, { entries=[entry]; universes=uctx } ) -> begin
     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), () = Future.force entry.Entries.const_entry_body in
+    let body = Future.force entry.const_entry_body in
+    let (body, cstr) = Safe_typing.inline_private_constants env body in
     let sigma = Evd.from_ctx uctx in
     let sigma = Evd.merge_context_set ~sideff:true Evd.univ_rigid sigma cstr in
     Inductiveops.control_only_guard (Global.env ()) sigma (EConstr.of_constr body);