Merge PR #10434: [declare] Fine tuning of Hook type.

Ack-by: ejgallego
Reviewed-by: ppedrot

1 files changed, 3 insertions, 3 deletions

diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 254760cb50..56ed406e2f 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -123,9 +123,9 @@ open DeclareDef
 
 let definition_message = Declare.definition_message
 
-let save id const ?hook uctx locality kind =
+let save id const ?hook uctx scope kind =
   let fix_exn = Future.fix_exn_of const.Proof_global.proof_entry_body in
-  let r = match locality with
+  let r = match scope with
     | Discharge ->
         let k = Kindops.logical_kind_of_goal_kind kind in
         let c = SectionLocalDef const in
@@ -136,7 +136,7 @@ let save id const ?hook uctx locality kind =
         let kn = declare_constant id ~local (Declare.DefinitionEntry const, k) in
         ConstRef kn
   in
-  DeclareDef.Hook.call ?hook ~fix_exn uctx [] locality r;
+  DeclareDef.Hook.(call ?hook ~fix_exn { S.uctx; obls = []; scope; dref = r });
   definition_message id
 
 let with_full_print f a =