1 files changed, 17 insertions, 0 deletions
diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml
index 92b7f2accf..570b72136c 100644
--- a/plugins/funind/gen_principle.ml
+++ b/plugins/funind/gen_principle.ml
@@ -234,6 +234,23 @@ let change_property_sort evd toSort princ princName =
     )
     (List.map (fun d -> Termops.map_rel_decl EConstr.Unsafe.to_constr d) princ_info.Tactics.params)
 
+(* XXX: To be cleaned up soon in favor of common save path. *)
+let save name const ?hook uctx scope kind =
+  let open Declare in
+  let open DeclareDef in
+  let fix_exn = Future.fix_exn_of const.Declare.proof_entry_body in
+  let r = match scope with
+    | Discharge ->
+      let c = SectionLocalDef const in
+      let () = declare_variable ~name ~kind c in
+      GlobRef.VarRef name
+    | Global local ->
+      let kn = declare_constant ~name ~kind ~local (DefinitionEntry const) in
+      GlobRef.ConstRef kn
+  in
+  DeclareDef.Hook.(call ?hook ~fix_exn { S.uctx; obls = []; scope; dref = r });
+  definition_message name
+
 let generate_functional_principle (evd: Evd.evar_map ref)
     interactive_proof
     old_princ_type sorts new_princ_name funs i proof_tac