[proof] Move declaration hooks to DeclareDef.

This way both `Lemmas` and `DeclareObl` can depend on it, removing one
more difficulty on the unification of terminators.

5 files changed, 6 insertions, 6 deletions

diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 8af5dc818b..08acb754f7 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -307,7 +307,7 @@ let build_functional_principle (evd:Evd.evar_map ref) interactive_proof old_prin
   in
   let sigma, _ = Typing.type_of ~refresh:true (Global.env ()) !evd (EConstr.of_constr new_principle_type) in
   evd := sigma;
-  let hook = Lemmas.mk_hook (hook new_principle_type) in
+  let hook = DeclareDef.Hook.make (hook new_principle_type) in
   let lemma =
     Lemmas.start_lemma
       new_princ_name
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 7683ce1757..732a0d818f 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -137,7 +137,7 @@ let save id const ?hook uctx (locality,_,kind) =
         let kn = declare_constant id ~local (DefinitionEntry const, k) in
         ConstRef kn
   in
-  Lemmas.call_hook ?hook ~fix_exn uctx [] locality r;
+  DeclareDef.Hook.call ?hook ~fix_exn uctx [] locality r;
   definition_message id
 
 let with_full_print f a =
diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli
index 4078c34331..8dd990775b 100644
--- a/plugins/funind/indfun_common.mli
+++ b/plugins/funind/indfun_common.mli
@@ -45,7 +45,7 @@ val jmeq_refl : unit -> EConstr.constr
 val save
   :  Id.t
   -> Evd.side_effects Entries.definition_entry
-  -> ?hook:Lemmas.declaration_hook
+  -> ?hook:DeclareDef.Hook.t
   -> UState.t
   -> Decl_kinds.goal_kind
   -> unit
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 2b5c0a01db..8169ff459f 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -1371,7 +1371,7 @@ let open_new_goal ~lemma build_proof sigma using_lemmas ref_ goal_name (gls_type
   let lemma = Lemmas.start_lemma
     na
     Decl_kinds.(Global ImportDefaultBehavior, false (* FIXME *), Proof Lemma)
-    sigma gls_type ~hook:(Lemmas.mk_hook hook) in
+    sigma gls_type ~hook:(DeclareDef.Hook.make hook) in
   let lemma = if Indfun_common.is_strict_tcc  ()
   then
     fst @@ Lemmas.by (Proofview.V82.tactic (tclIDTAC)) lemma
@@ -1592,5 +1592,5 @@ let recursive_definition ~interactive_proof ~is_mes function_name rec_impls type
         term_id
         using_lemmas
         (List.length res_vars)
-        evd (Lemmas.mk_hook hook))
+        evd (DeclareDef.Hook.make hook))
     ()
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 2da6584aba..2bab55ef74 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -2006,7 +2006,7 @@ let add_morphism_interactive atts m n : Lemmas.t =
       declare_projection n instance_id (ConstRef cst)
     | _ -> assert false
   in
-  let hook = Lemmas.mk_hook hook in
+  let hook = DeclareDef.Hook.make hook in
   Flags.silently
     (fun () ->
        let lemma = Lemmas.start_lemma ~hook instance_id kind (Evd.from_ctx uctx) (EConstr.of_constr instance) in