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

Ack-by: ejgallego
Reviewed-by: ppedrot

14 files changed, 77 insertions, 59 deletions

diff --git a/dev/ci/user-overlays/10434-ejgallego-proof+hook_record.sh b/dev/ci/user-overlays/10434-ejgallego-proof+hook_record.sh
new file mode 100644
index 0000000000..3a2f4e1001
--- /dev/null
+++ b/dev/ci/user-overlays/10434-ejgallego-proof+hook_record.sh
@@ -0,0 +1,12 @@
+if [ "$CI_PULL_REQUEST" = "10434" ] || [ "$CI_BRANCH" = "proof+hook_record" ]; then
+
+    equations_CI_REF=proof+hook_record
+    equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations
+
+    mtac2_CI_REF=proof+hook_record
+    mtac2_CI_GITURL=https://github.com/ejgallego/Mtac2
+
+    paramcoq_CI_REF=proof+hook_record
+    paramcoq_CI_GITURL=https://github.com/ejgallego/paramcoq
+
+fi
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 b68b31c93b..d38e28c0e7 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
diff --git a/vernac/class.ml b/vernac/class.ml
index febe8e34e4..6dba134764 100644
--- a/vernac/class.ml
+++ b/vernac/class.ml
@@ -355,27 +355,27 @@ let try_add_new_identity_coercion id ~local ~poly ~source ~target =
 let try_add_new_coercion_with_source ref ~local ~poly ~source =
   try_add_new_coercion_core ref ~local poly (Some source) None false
 
-let add_coercion_hook poly _uctx _trans local ref =
+let add_coercion_hook poly { DeclareDef.Hook.S.scope; dref; _ } =
   let open DeclareDef in
-  let local = match local with
+  let local = match scope with
   | Discharge -> assert false (* Local Coercion in section behaves like Local Definition *)
   | Global ImportNeedQualified -> true
   | Global ImportDefaultBehavior -> false
   in
-  let () = try_add_new_coercion ref ~local ~poly in
-  let msg = Nametab.pr_global_env Id.Set.empty ref ++ str " is now a coercion" in
+  let () = try_add_new_coercion dref ~local ~poly in
+  let msg = Nametab.pr_global_env Id.Set.empty dref ++ str " is now a coercion" in
   Flags.if_verbose Feedback.msg_info msg
 
 let add_coercion_hook ~poly = DeclareDef.Hook.make (add_coercion_hook poly)
 
-let add_subclass_hook ~poly _uctx _trans local ref =
+let add_subclass_hook ~poly { DeclareDef.Hook.S.scope; dref; _ } =
   let open DeclareDef in
-  let stre = match local with
+  let stre = match scope with
   | Discharge -> assert false (* Local Subclass in section behaves like Local Definition *)
   | Global ImportNeedQualified -> true
   | Global ImportDefaultBehavior -> false
   in
-  let cl = class_of_global ref in
+  let cl = class_of_global dref in
   try_add_new_coercion_subclass cl ~local:stre ~poly
 
 let add_subclass_hook ~poly = DeclareDef.Hook.make (add_subclass_hook ~poly)
diff --git a/vernac/classes.ml b/vernac/classes.ml
index 35108744cd..fbcd1744a8 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -343,9 +343,9 @@ let do_declare_instance sigma ~global ~poly k u ctx ctx' pri decl imps subst id
   instance_hook pri global imps (ConstRef cst)
 
 let declare_instance_program env sigma ~global ~poly id pri imps decl term termtype =
-  let hook _ _ vis gr =
-    let cst = match gr with ConstRef kn -> kn | _ -> assert false in
-    Impargs.declare_manual_implicits false gr imps;
+  let hook { DeclareDef.Hook.S.scope; dref; _ } =
+    let cst = match dref with ConstRef kn -> kn | _ -> assert false in
+    Impargs.declare_manual_implicits false dref imps;
     let pri = intern_info pri in
     let env = Global.env () in
     let sigma = Evd.from_env env in
@@ -374,7 +374,7 @@ let declare_instance_open sigma ?hook ~tac ~global ~poly id pri imps udecl ids t
   let sigma = Evd.reset_future_goals sigma in
   let scope = DeclareDef.Global Declare.ImportDefaultBehavior in
   let kind = Decl_kinds.DefinitionBody Decl_kinds.Instance in
-  let hook = DeclareDef.Hook.make (fun _ _ _ -> instance_hook pri global imps ?hook) in
+  let hook = DeclareDef.Hook.(make (fun { S.dref ; _ } -> instance_hook pri global imps ?hook dref)) in
   let info = Lemmas.Info.make ~hook ~scope ~kind () in
   let lemma = Lemmas.start_lemma ~name:id ~poly ~udecl ~info sigma (EConstr.of_constr termtype) in
   (* spiwack: I don't know what to do with the status here. *)
diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml
index d804957917..3947bb1b14 100644
--- a/vernac/comProgramFixpoint.ml
+++ b/vernac/comProgramFixpoint.ml
@@ -204,8 +204,8 @@ let build_wellfounded (recname,pl,bl,arityc,body) poly r measure notation =
       let name = add_suffix recname "_func" in
       (* XXX: Mutating the evar_map in the hook! *)
       (* XXX: Likely the sigma is out of date when the hook is called .... *)
-      let hook sigma _ _ l gr =
-        let sigma, h_body = Evarutil.new_global sigma gr in
+      let hook sigma { DeclareDef.Hook.S.dref; _ } =
+        let sigma, h_body = Evarutil.new_global sigma dref in
         let body = it_mkLambda_or_LetIn (mkApp (h_body, [|make|])) binders_rel in
         let ty = it_mkProd_or_LetIn top_arity binders_rel in
         let ty = EConstr.Unsafe.to_constr ty in
@@ -222,9 +222,9 @@ let build_wellfounded (recname,pl,bl,arityc,body) poly r measure notation =
       hook, name, typ
     else
       let typ = it_mkProd_or_LetIn top_arity binders_rel in
-      let hook sigma _ _ l gr =
+      let hook sigma { DeclareDef.Hook.S.dref; _ } =
         if Impargs.is_implicit_args () || not (List.is_empty impls) then
-          Impargs.declare_manual_implicits false gr impls
+          Impargs.declare_manual_implicits false dref impls
       in hook, recname, typ
   in
   (* XXX: Capturing sigma here... bad bad *)
diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml
index d74fdcab2c..d229973936 100644
--- a/vernac/declareDef.ml
+++ b/vernac/declareDef.ml
@@ -18,19 +18,26 @@ type locality = Discharge | Global of Declare.import_status
 (* Hooks naturally belong here as they apply to both definitions and lemmas *)
 module Hook = struct
   module S = struct
-    type t = UState.t
-      -> (Names.Id.t * Constr.t) list
-      -> locality
-      -> Names.GlobRef.t
-      -> unit
+    type t =
+      { uctx : UState.t
+      (** [ustate]: universe constraints obtained when the term was closed *)
+      ; obls : (Names.Id.t * Constr.t) list
+      (** [(n1,t1),...(nm,tm)]: association list between obligation
+          name and the corresponding defined term (might be a constant,
+          but also an arbitrary term in the Expand case of obligations) *)
+      ; scope : locality
+      (**  [locality]: Locality of the original declaration *)
+      ; dref : Names.GlobRef.t
+      (** [ref]: identifier of the original declaration *)
+      }
   end
 
-  type t = S.t CEphemeron.key
+  type t = (S.t -> unit) CEphemeron.key
 
   let make hook = CEphemeron.create hook
 
-  let call ?hook ?fix_exn uctx trans l c =
-    try Option.iter (fun hook -> CEphemeron.get hook uctx trans l c) hook
+  let call ?hook ?fix_exn x =
+    try Option.iter (fun hook -> CEphemeron.get hook x) hook
     with e when CErrors.noncritical e ->
       let e = CErrors.push e in
       let e = Option.cata (fun fix -> fix e) e fix_exn in
@@ -55,8 +62,8 @@ let declare_definition ~name ~scope ~kind ?hook_data udecl ce imps =
   begin
     match hook_data with
     | None -> ()
-    | Some (hook, uctx, extra_defs) ->
-      Hook.call ~fix_exn ~hook uctx extra_defs scope gr
+    | Some (hook, uctx, obls) ->
+      Hook.call ~fix_exn ~hook { Hook.S.uctx; obls; scope; dref = gr }
   end;
   gr
 
diff --git a/vernac/declareDef.mli b/vernac/declareDef.mli
index 3934a29413..cfff89bc34 100644
--- a/vernac/declareDef.mli
+++ b/vernac/declareDef.mli
@@ -22,23 +22,22 @@ module Hook : sig
      as a Coercion, perform some cleanup, update the search database,
      etc...  *)
   module S : sig
-    (** [S.t] passes to the client: *)
-    type t
-      =  UState.t
+    type t =
+      { uctx : UState.t
       (** [ustate]: universe constraints obtained when the term was closed *)
-      -> (Id.t * Constr.t) list
+      ; obls : (Id.t * Constr.t) list
       (** [(n1,t1),...(nm,tm)]: association list between obligation
           name and the corresponding defined term (might be a constant,
           but also an arbitrary term in the Expand case of obligations) *)
-      -> locality
-      (**  [locality]: Locality of the original declaration *)
-      -> GlobRef.t
-      (** [ref]: identifier of the original declaration *)
-      -> unit
+      ; scope : locality
+      (** [scope]: Locality of the original declaration *)
+      ; dref : GlobRef.t
+      (** [dref]: identifier of the original declaration *)
+      }
   end
 
-  val make : S.t -> t
-  val call : ?hook:t -> ?fix_exn:Future.fix_exn -> S.t
+  val make : (S.t -> unit) -> t
+  val call : ?hook:t -> ?fix_exn:Future.fix_exn -> S.t -> unit
 end
 
 val declare_definition
diff --git a/vernac/declareObl.ml b/vernac/declareObl.ml
index 759e907bc9..cd521255a0 100644
--- a/vernac/declareObl.ml
+++ b/vernac/declareObl.ml
@@ -455,10 +455,10 @@ let declare_mutual_definition l =
     (Metasyntax.add_notation_interpretation (Global.env ()))
     first.prg_notations;
   Declare.recursive_message (fixkind != IsCoFixpoint) indexes fixnames;
-  let gr = List.hd kns in
-  DeclareDef.Hook.call ?hook:first.prg_hook ~fix_exn first.prg_ctx obls scope gr;
+  let dref = List.hd kns in
+  DeclareDef.Hook.(call ?hook:first.prg_hook ~fix_exn { S.uctx = first.prg_ctx; obls; scope; dref });
   List.iter progmap_remove l;
-  gr
+  dref
 
 let update_obls prg obls rem =
   let prg' = {prg with prg_obligations = (obls, rem)} in
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 31407de4da..e586200ba3 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -421,19 +421,19 @@ let warn_let_as_axiom =
 
 (* This declares implicits and calls the hooks for all the theorems,
    including the main one *)
-let process_recthms ?fix_exn ?hook env sigma ctx ~udecl ~poly ~scope ref imps other_thms =
+let process_recthms ?fix_exn ?hook env sigma uctx ~udecl ~poly ~scope dref imps other_thms =
   let other_thms_data =
     if List.is_empty other_thms then [] else
       (* there are several theorems defined mutually *)
-      let body,opaq = retrieve_first_recthm ctx ref in
-      let norm c = EConstr.to_constr (Evd.from_ctx ctx) c in
+      let body,opaq = retrieve_first_recthm uctx dref in
+      let norm c = EConstr.to_constr (Evd.from_ctx uctx) c in
       let body = Option.map EConstr.of_constr body in
-      let uctx = UState.check_univ_decl ~poly ctx udecl in
+      let uctx = UState.check_univ_decl ~poly uctx udecl in
       List.map_i (save_remaining_recthms env sigma ~poly ~scope norm uctx body opaq) 1 other_thms in
-  let thms_data = (ref,imps)::other_thms_data in
-  List.iter (fun (ref,imps) ->
-      maybe_declare_manual_implicits false ref imps;
-      DeclareDef.Hook.call ?fix_exn ?hook ctx [] scope ref) thms_data
+  let thms_data = (dref,imps)::other_thms_data in
+  List.iter (fun (dref,imps) ->
+      maybe_declare_manual_implicits false dref imps;
+      DeclareDef.Hook.(call ?fix_exn ?hook { S.uctx; obls = []; scope; dref})) thms_data
 
 let get_keep_admitted_vars =
   Goptions.declare_bool_option_and_ref
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index b7392a28ca..e82694b740 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -441,9 +441,9 @@ let solve_by_tac ?loc name evi t poly ctx =
     warn_solve_errored ?loc err;
     None
 
-let obligation_hook prg obl num auto ctx' _ _ gr =
+let obligation_hook prg obl num auto { DeclareDef.Hook.S.uctx = ctx'; dref; _ } =
   let obls, rem = prg.prg_obligations in
-  let cst = match gr with GlobRef.ConstRef cst -> cst | _ -> assert false in
+  let cst = match dref with GlobRef.ConstRef cst -> cst | _ -> assert false in
   let transparent = evaluable_constant cst (Global.env ()) in
   let () = match obl.obl_status with
       (true, Evar_kinds.Expand)
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index e0183b941e..b07a5d259d 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -578,7 +578,7 @@ let vernac_definition_hook ~poly = function
 | Coercion ->
   Some (Class.add_coercion_hook ~poly)
 | CanonicalStructure ->
-  Some (DeclareDef.Hook.make (fun _ _ _ -> Canonical.declare_canonical_structure))
+  Some (DeclareDef.Hook.(make (fun { S.dref } -> Canonical.declare_canonical_structure dref)))
 | SubClass ->
   Some (Class.add_subclass_hook ~poly)
 | _ -> None