[declare] Fine tuning of Hook type.

We turn the hook parameter into a record, making more explicit the
capture of data in hooks as they only take one parameter now

This is a fine-tuning but provides some small advantages, and allows
us to tweak the hook type with less breakage.

4 files changed, 9 insertions, 9 deletions

diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index edda2f2eef..3bab750534 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -354,7 +354,7 @@ let generate_functional_principle (evd: Evd.evar_map ref)
   in
   let names = ref [new_princ_name] in
   let hook =
-    fun new_principle_type _ _ _ _  ->
+    fun new_principle_type _  ->
     if Option.is_empty sorts
     then
       (*     let id_of_f = Label.to_id (con_label f) in *)
@@ -526,7 +526,7 @@ let make_scheme evd (fas : (pconstant*Sorts.family) list) : Evd.side_effects Pro
         this_block_funs
         0
         (prove_princ_for_struct evd false 0 (Array.of_list (List.map fst funs)))
-        (fun _ _ _ _ _ -> ())
+        (fun _ _ -> ())
     with e when CErrors.noncritical e ->
       raise (Defining_principle e)
 
@@ -588,7 +588,7 @@ let make_scheme evd (fas : (pconstant*Sorts.family) list) : Evd.side_effects Pro
                  this_block_funs
                  !i
                  (prove_princ_for_struct evd false !i (Array.of_list (List.map fst funs)))
-                 (fun _ _ _ _ _ -> ())
+                 (fun _ _ -> ())
              in
              const
          with Found_type i ->
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 =
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 425e498330..150a4a6249 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -1308,7 +1308,7 @@ let open_new_goal ~lemma build_proof sigma using_lemmas ref_ goal_name (gls_type
   let na = next_global_ident_away name Id.Set.empty in
   if Termops.occur_existential sigma gls_type then
     CErrors.user_err Pp.(str "\"abstract\" cannot handle existentials");
-  let hook _ _ _ _ =
+  let hook _ =
     let opacity =
       let na_ref = qualid_of_ident na in
       let na_global = Smartlocate.global_with_alias na_ref in
@@ -1547,7 +1547,7 @@ let recursive_definition ~interactive_proof ~is_mes function_name rec_impls type
   let tcc_lemma_name = add_suffix function_name "_tcc" in
   let tcc_lemma_constr = ref Undefined in
   (* let _ = Pp.msgnl (fun _ _ -> str "relation := " ++ Printer.pr_lconstr_env env_with_pre_rec_args relation) in *)
-  let hook uctx _ _ _ =
+  let hook { DeclareDef.Hook.S.uctx ; _ } =
     let term_ref = Nametab.locate (qualid_of_ident term_id) in
     let f_ref = declare_f function_name (IsProof Lemma) arg_types term_ref in
     let _ = Extraction_plugin.Table.extraction_inline true [qualid_of_ident term_id] in
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 8acb29ba74..19866df8e3 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -1997,7 +1997,7 @@ let add_morphism_interactive atts m n : Lemmas.t =
   let poly = atts.polymorphic in
   let kind = Decl_kinds.DefinitionBody Decl_kinds.Instance in
   let tac = make_tactic "Coq.Classes.SetoidTactics.add_morphism_tactic" in
-  let hook _ _ _ = function
+  let hook { DeclareDef.Hook.S.dref; _ } = dref |> function
     | Globnames.ConstRef cst ->
       Classes.add_instance (Classes.mk_instance
                       (PropGlobal.proper_class env evd) Hints.empty_hint_info