3 files changed, 17 insertions, 32 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
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 6d91c2a348..80fc64fe65 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -107,29 +107,6 @@ let find_reference sl s =
 let eq = lazy(EConstr.of_constr (coq_constant "eq"))
 let refl_equal = lazy(EConstr.of_constr (coq_constant "eq_refl"))
 
-(*****************************************************************)
-(* Copy of the standard save mechanism but without the much too  *)
-(* slow reduction function                                       *)
-(*****************************************************************)
-open Declare
-open DeclareDef
-
-let definition_message = Declare.definition_message
-
-let save name const ?hook uctx scope kind =
-  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 with_full_print f a =
   let old_implicit_args = Impargs.is_implicit_args ()
   and old_strict_implicit_args =  Impargs.is_strict_implicit_args ()
diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli
index 34fb10bb67..cd5202a6c7 100644
--- a/plugins/funind/indfun_common.mli
+++ b/plugins/funind/indfun_common.mli
@@ -42,15 +42,6 @@ val jmeq : unit -> EConstr.constr
 val jmeq_refl : unit -> EConstr.constr
 val make_eq : unit -> EConstr.constr
 
-val save
-  :  Id.t
-  -> Evd.side_effects Declare.proof_entry
-  -> ?hook:DeclareDef.Hook.t
-  -> UState.t
-  -> DeclareDef.locality
-  -> Decls.logical_kind
-  -> unit
-
 (* [with_full_print f a] applies [f] to [a] in full printing environment.
 
    This function preserves the print settings