[declare] Provide helper for private constant inlining.

We factor some duplicate code, this is a step towards making the
`proof_entry` type abstract.

5 files changed, 25 insertions, 13 deletions

diff --git a/tactics/declare.ml b/tactics/declare.ml
index 57eeddb847..dcbd28f829 100644
--- a/tactics/declare.ml
+++ b/tactics/declare.ml
@@ -326,6 +326,12 @@ let declare_private_constant ?role ?(local = ImportDefaultBehavior) ~name ~kind
   let eff = { Evd.seff_private = eff; Evd.seff_roles; } in
   kn, eff
 
+let inline_private_constants ~univs env ce =
+  let body, eff = Future.force ce.proof_entry_body in
+  let cb, ctx = Safe_typing.inline_private_constants env (body, eff.Evd.seff_private) in
+  let univs = UState.merge ~sideff:true Evd.univ_rigid univs ctx in
+  cb, univs
+
 (** Declaration of section variables and local definitions *)
 type variable_declaration =
   | SectionLocalDef of Evd.side_effects proof_entry
diff --git a/tactics/declare.mli b/tactics/declare.mli
index 1a037ef937..439f0018aa 100644
--- a/tactics/declare.mli
+++ b/tactics/declare.mli
@@ -83,6 +83,15 @@ val declare_private_constant
   -> unit proof_entry
   -> Constant.t * Evd.side_effects
 
+(** [inline_private_constants ~sideff ~univs env ce] will inline the
+   constants in [ce]'s body and return the body plus the updated
+   [UState.t]. *)
+val inline_private_constants
+  :  univs:UState.t
+  -> Environ.env
+  -> Evd.side_effects proof_entry
+  -> Constr.t * UState.t
+
 (** Since transparent constants' side effects are globally declared, we
  *  need that *)
 val set_declare_scheme :
diff --git a/tactics/pfedit.ml b/tactics/pfedit.ml
index 413c6540a3..c470ea04c7 100644
--- a/tactics/pfedit.ml
+++ b/tactics/pfedit.ml
@@ -135,12 +135,13 @@ let build_by_tactic ?(side_eff=true) env sigma ~poly typ tac =
   let name = Id.of_string ("temporary_proof"^string_of_int (next())) in
   let sign = val_of_named_context (named_context env) in
   let ce, status, univs = build_constant_by_tactic ~name sigma sign ~poly typ tac in
-  let body, eff = Future.force ce.Declare.proof_entry_body in
-  let (cb, ctx) =
-    if side_eff then Safe_typing.inline_private_constants env (body, eff.Evd.seff_private)
-    else body
+  let cb, univs =
+    if side_eff then Declare.inline_private_constants ~univs env ce
+    else
+      (* GG: side effects won't get reset: no need to treat their universes specially *)
+      let (cb, ctx), _eff = Future.force ce.Declare.proof_entry_body in
+      cb, UState.merge ~sideff:false Evd.univ_rigid univs ctx
   in
-  let univs = UState.merge ~sideff:side_eff Evd.univ_rigid univs ctx in
   cb, status, univs
 
 let refine_by_tactic ~name ~poly env sigma ty tac =
diff --git a/vernac/declareObl.ml b/vernac/declareObl.ml
index 2c56f707f1..b56b9c8ce2 100644
--- a/vernac/declareObl.ml
+++ b/vernac/declareObl.ml
@@ -490,10 +490,8 @@ let obligation_terminator entries uctx { name; num; auto } =
   | [entry] ->
     let env = Global.env () in
     let ty = entry.Declare.proof_entry_type in
-    let body, eff = Future.force entry.Declare.proof_entry_body in
-    let (body, cstr) = Safe_typing.inline_private_constants env (body, eff.Evd.seff_private) in
+    let body, uctx = Declare.inline_private_constants ~univs:uctx env entry 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);
     (* Declare the obligation ourselves and drop the hook *)
     let prg = CEphemeron.get (ProgMap.find name !from_prg) in
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index c8cede1f84..4ea34e2b60 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -423,11 +423,9 @@ let solve_by_tac ?loc name evi t poly ctx =
       Pfedit.build_constant_by_tactic
         ~name ~poly ctx evi.evar_hyps evi.evar_concl t in
     let env = Global.env () in
-    let (body, eff) = Future.force entry.Declare.proof_entry_body in
-    let body = Safe_typing.inline_private_constants env (body, eff.Evd.seff_private) 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.Declare.proof_entry_type, Evd.evar_universe_context ctx')
+    let body, ctx' = Declare.inline_private_constants ~univs:ctx' env entry in
+    Inductiveops.control_only_guard env (Evd.from_ctx ctx') (EConstr.of_constr body);
+    Some (body, entry.Declare.proof_entry_type, ctx')
   with
   | Refiner.FailError (_, s) as exn ->
     let _ = CErrors.push exn in