From 4035b4a66dbd8e29aa933b1e301fbd07815768e4 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Fri, 25 Oct 2019 00:31:36 +0200
Subject: [funind] Remove duplicate save function.

AFAICT the reasoning for introducing this function doesn't hold
anymore. This is needed for future refactorings that should make some
types private.
---
 plugins/funind/gen_principle.ml | 26 ++++++++------------------
 1 file changed, 8 insertions(+), 18 deletions(-)

(limited to 'plugins')

diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml
index 6011af74e5..0452665585 100644
--- a/plugins/funind/gen_principle.ml
+++ b/plugins/funind/gen_principle.ml
@@ -234,23 +234,6 @@ 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
@@ -307,7 +290,14 @@ let generate_functional_principle (evd: Evd.evar_map ref)
      Don't forget to close the goal if an error is raised !!!!
   *)
   let uctx = Evd.evar_universe_context sigma in
-  save new_princ_name entry ~hook uctx (DeclareDef.Global Declare.ImportDefaultBehavior) Decls.(IsProof Theorem)
+  let hook_data = hook, uctx, [] in
+  let _ : Names.GlobRef.t = DeclareDef.declare_definition
+      ~name:new_princ_name ~hook_data
+      ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior)
+      ~kind:Decls.(IsProof Theorem)
+      UnivNames.empty_binders
+      entry [] in
+  ()
   with e when CErrors.noncritical e ->
     raise (Defining_principle e)
 
-- 
cgit v1.2.3