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

Ack-by: ejgallego
Reviewed-by: ppedrot

9 files changed, 56 insertions, 50 deletions

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