Merge PR #10949: [declare] Provide helper for private constant inlining.

Reviewed-by: SkySkimmer
Reviewed-by: ppedrot

3 files changed, 21 insertions, 5 deletions

diff --git a/tactics/declare.ml b/tactics/declare.ml
index 4ef0fb9459..9f104590e7 100644
--- a/tactics/declare.ml
+++ b/tactics/declare.ml
@@ -347,6 +347,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 c9cad823a4..a4d3f17594 100644
--- a/tactics/declare.mli
+++ b/tactics/declare.mli
@@ -108,6 +108,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 c336cd1edd..3c9803432a 100644
--- a/tactics/pfedit.ml
+++ b/tactics/pfedit.ml
@@ -138,12 +138,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 =