Merge PR #9645: [proof] Remove terminator type, unifying regular and obligation ones.

Ack-by: ejgallego
Ack-by: gares
Reviewed-by: ppedrot

4 files changed, 5 insertions, 5 deletions

diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 2fe1d1ff40..48eac96ab3 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 1ee5407bcc..b049e3607c 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))
     ()