Merge PR #8704: [vernac] Remove unused abstraction from declaration_hook type.

14 files changed, 68 insertions, 44 deletions

diff --git a/dev/ci/user-overlays/08704-ejgallego-vernac+monify_hook.sh b/dev/ci/user-overlays/08704-ejgallego-vernac+monify_hook.sh
new file mode 100644
index 0000000000..b3a9f67e00
--- /dev/null
+++ b/dev/ci/user-overlays/08704-ejgallego-vernac+monify_hook.sh
@@ -0,0 +1,15 @@
+if [ "$CI_PULL_REQUEST" = "8704" ] || [ "$CI_BRANCH" = "vernac+monify_hook" ]; then
+
+    # ltac2_CI_REF=rm-section-path
+    # ltac2_CI_GITURL=https://github.com/maximedenes/ltac2
+
+    plugin_tutorial_CI_REF=vernac+monify_hook
+    plugin_tutorial_CI_GITURL=https://github.com/ejgallego/plugin_tutorials
+
+    Elpi_CI_REF=vernac+monify_hook
+    Elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi
+
+    Equations_CI_REF=vernac+monify_hook
+    Equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations
+
+fi
diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli
index 7e52ee224f..1b4c1248a5 100644
--- a/plugins/funind/indfun_common.mli
+++ b/plugins/funind/indfun_common.mli
@@ -46,7 +46,7 @@ val jmeq : unit -> EConstr.constr
 val jmeq_refl : unit -> EConstr.constr
 
 val save : bool -> Id.t -> Safe_typing.private_constants Entries.definition_entry  -> Decl_kinds.goal_kind ->
-  unit Lemmas.declaration_hook CEphemeron.key -> unit
+  Lemmas.declaration_hook CEphemeron.key -> unit
 
 (* [get_proof_clean do_reduce] : returns the proof name, definition, kind and hook and
    abort the proof
diff --git a/vernac/class.mli b/vernac/class.mli
index f7e837f3bb..80d6d4383c 100644
--- a/vernac/class.mli
+++ b/vernac/class.mli
@@ -42,8 +42,8 @@ val try_add_new_coercion_with_source : GlobRef.t -> local:bool ->
 val try_add_new_identity_coercion : Id.t -> local:bool -> 
   Decl_kinds.polymorphic -> source:cl_typ -> target:cl_typ -> unit
 
-val add_coercion_hook : Decl_kinds.polymorphic -> unit Lemmas.declaration_hook
+val add_coercion_hook : Decl_kinds.polymorphic -> Lemmas.declaration_hook
 
-val add_subclass_hook : Decl_kinds.polymorphic -> unit Lemmas.declaration_hook
+val add_subclass_hook : Decl_kinds.polymorphic -> Lemmas.declaration_hook
 
 val class_of_global : GlobRef.t -> cl_typ
diff --git a/vernac/classes.ml b/vernac/classes.ml
index 37ee33b19f..09e2b8df45 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -149,7 +149,7 @@ let do_abstract_instance env sigma ?hook ~global ~poly k u ctx ctx' pri decl imp
 let declare_instance_open env sigma ?hook ~tac ~program_mode ~global ~poly k id pri imps decl len term termtype =
   let kind = Decl_kinds.Global, poly, Decl_kinds.DefinitionBody Decl_kinds.Instance in
   if program_mode then
-    let hook vis gr _ =
+    let hook _ vis gr =
       let cst = match gr with ConstRef kn -> kn | _ -> assert false in
       Impargs.declare_manual_implicits false gr ~enriching:false [imps];
       let pri = intern_info pri in
@@ -163,7 +163,7 @@ let declare_instance_open env sigma ?hook ~tac ~program_mode ~global ~poly k id
         in obls, Some constr, typ
       | None -> [||], None, termtype
     in
-    let hook = Lemmas.mk_hook hook in
+    let hook = Obligations.mk_univ_hook hook in
     let ctx = Evd.evar_universe_context sigma in
     ignore (Obligations.add_definition id ?term:constr
               ~univdecl:decl typ ctx ~kind:(Global,poly,Instance) ~hook obls)
@@ -425,7 +425,7 @@ let context poly l =
       | Some b ->
         let decl = (Discharge, poly, Definition) in
         let entry = Declare.definition_entry ~univs ~types:t b in
-        let hook = Lemmas.mk_hook (fun _ gr -> gr) in
+        let hook = Lemmas.mk_hook (fun _ _ -> ()) in
         let _ = DeclareDef.declare_definition id decl entry UnivNames.empty_binders [] hook in
         Lib.sections_are_opened () || Lib.is_modtype_strict ()
       in
diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml
index a8d7946429..5d17662d1a 100644
--- a/vernac/comDefinition.ml
+++ b/vernac/comDefinition.ml
@@ -127,10 +127,8 @@ let do_definition ~program_mode ident k univdecl bl red_option c ctypopt hook =
         Obligations.eterm_obligations env ident evd 0 c typ
       in
       let ctx = Evd.evar_universe_context evd in
-      let hook = Lemmas.mk_hook (fun l r _ -> Lemmas.call_hook (fun exn -> exn) hook l r) in
+      let hook = Obligations.mk_univ_hook (fun _ l r -> Lemmas.call_hook (fun x -> x) hook l r) in
       ignore(Obligations.add_definition
           ident ~term:c cty ctx ~univdecl ~implicits:imps ~kind:k ~hook obls)
     else let ce = check_definition def in
-      ignore(DeclareDef.declare_definition ident k ce (Evd.universe_binders evd) imps
-        (Lemmas.mk_hook
-          (fun l r -> Lemmas.call_hook (fun exn -> exn) hook l r;r)))
+      ignore(DeclareDef.declare_definition ident k ce (Evd.universe_binders evd) imps hook)
diff --git a/vernac/comDefinition.mli b/vernac/comDefinition.mli
index 7f1c902c0f..58007e6a88 100644
--- a/vernac/comDefinition.mli
+++ b/vernac/comDefinition.mli
@@ -19,7 +19,7 @@ open Constrexpr
 val do_definition : program_mode:bool ->
   Id.t -> definition_kind -> universe_decl_expr option ->
   local_binder_expr list -> red_expr option -> constr_expr ->
-  constr_expr option -> unit Lemmas.declaration_hook -> unit
+  constr_expr option -> Lemmas.declaration_hook -> unit
 
 (************************************************************************)
 (** Internal API  *)
diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml
index c33e6b72c6..ab898644c0 100644
--- a/vernac/comProgramFixpoint.ml
+++ b/vernac/comProgramFixpoint.ml
@@ -192,7 +192,7 @@ let build_wellfounded (recname,pl,n,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 hook sigma _ l gr =
         let sigma, h_body = Evarutil.new_global sigma gr 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
@@ -211,13 +211,13 @@ let build_wellfounded (recname,pl,n,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 _ l gr =
         if Impargs.is_implicit_args () || not (List.is_empty impls) then
           Impargs.declare_manual_implicits false gr [impls]
       in hook, recname, typ
   in
   (* XXX: Capturing sigma here... bad bad *)
-  let hook = Lemmas.mk_hook (hook sigma) in
+  let hook = Obligations.mk_univ_hook (hook sigma) in
   (* XXX: Grounding non-ground terms here... bad bad *)
   let fullcoqc = EConstr.to_constr ~abort_on_undefined_evars:false sigma def in
   let fullctyp = EConstr.to_constr sigma typ in
diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml
index 77177dfa41..7426c128cc 100644
--- a/vernac/declareDef.ml
+++ b/vernac/declareDef.ml
@@ -58,9 +58,9 @@ let declare_definition ident (local, p, k) ce pl imps hook =
     gr
   | Discharge | Local | Global ->
     declare_global_definition ident ce local k pl imps in
-  Lemmas.call_hook fix_exn hook local r
+  Lemmas.call_hook fix_exn hook local r; r
 
 let declare_fix ?(opaque = false) (_,poly,_ as kind) pl univs f ((def,_),eff) t imps =
   let ce = definition_entry ~opaque ~types:t ~univs ~eff def in
-  declare_definition f kind ce pl imps (Lemmas.mk_hook (fun _ r -> r))
+  declare_definition f kind ce pl imps (Lemmas.mk_hook (fun _ _ -> ()))
 
diff --git a/vernac/declareDef.mli b/vernac/declareDef.mli
index c5e704a5e9..da11d4d9c0 100644
--- a/vernac/declareDef.mli
+++ b/vernac/declareDef.mli
@@ -15,7 +15,7 @@ val get_locality : Id.t -> kind:string -> Decl_kinds.locality -> bool
 
 val declare_definition : Id.t -> definition_kind ->
   Safe_typing.private_constants Entries.definition_entry -> UnivNames.universe_binders -> Impargs.manual_implicits ->
-    GlobRef.t Lemmas.declaration_hook -> GlobRef.t
+  Lemmas.declaration_hook -> GlobRef.t
 
 val declare_fix : ?opaque:bool -> definition_kind ->
   UnivNames.universe_binders -> Entries.constant_universes_entry ->
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index bbefd2dfe7..a99aace399 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -34,7 +34,7 @@ open Impargs
 module RelDecl = Context.Rel.Declaration
 module NamedDecl = Context.Named.Declaration
 
-type 'a declaration_hook = Decl_kinds.locality -> GlobRef.t -> 'a
+type declaration_hook = Decl_kinds.locality -> GlobRef.t -> unit
 let mk_hook hook = hook
 let call_hook fix_exn hook l c =
   try hook l c
diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli
index d8e337c09c..195fcbf4ca 100644
--- a/vernac/lemmas.mli
+++ b/vernac/lemmas.mli
@@ -11,44 +11,41 @@
 open Names
 open Decl_kinds
 
-type 'a declaration_hook
-val mk_hook :
-  (Decl_kinds.locality -> GlobRef.t -> 'a) -> 'a declaration_hook
-
-val call_hook :
-  Future.fix_exn -> 'a declaration_hook -> Decl_kinds.locality -> GlobRef.t -> 'a
+type declaration_hook
+val mk_hook : (Decl_kinds.locality -> GlobRef.t -> unit) -> declaration_hook
+val call_hook : Future.fix_exn -> declaration_hook -> Decl_kinds.locality -> GlobRef.t -> unit
 
 val start_proof : Id.t -> ?pl:UState.universe_decl -> goal_kind -> Evd.evar_map ->
-  ?terminator:(Proof_global.lemma_possible_guards -> unit declaration_hook -> Proof_global.proof_terminator) ->
+  ?terminator:(Proof_global.lemma_possible_guards -> declaration_hook -> Proof_global.proof_terminator) ->
   ?sign:Environ.named_context_val -> EConstr.types ->
-  ?init_tac:unit Proofview.tactic -> ?compute_guard:Proof_global.lemma_possible_guards -> 
-   unit declaration_hook -> unit
+  ?init_tac:unit Proofview.tactic -> ?compute_guard:Proof_global.lemma_possible_guards ->
+  declaration_hook -> unit
 
 val start_proof_univs : Id.t -> ?pl:UState.universe_decl -> goal_kind -> Evd.evar_map ->
-  ?terminator:(Proof_global.lemma_possible_guards -> (UState.t option -> unit declaration_hook) -> Proof_global.proof_terminator) ->
+  ?terminator:(Proof_global.lemma_possible_guards -> (UState.t option -> declaration_hook) -> Proof_global.proof_terminator) ->
   ?sign:Environ.named_context_val -> EConstr.types ->
-  ?init_tac:unit Proofview.tactic -> ?compute_guard:Proof_global.lemma_possible_guards -> 
-  (UState.t option -> unit declaration_hook) -> unit
+  ?init_tac:unit Proofview.tactic -> ?compute_guard:Proof_global.lemma_possible_guards ->
+  (UState.t option -> declaration_hook) -> unit
 
 val start_proof_com :
   ?inference_hook:Pretyping.inference_hook ->
   goal_kind -> Vernacexpr.proof_expr list ->
-  unit declaration_hook -> unit
+  declaration_hook -> unit
 
 val start_proof_with_initialization :
   goal_kind -> Evd.evar_map -> UState.universe_decl ->
   (bool * Proof_global.lemma_possible_guards * unit Proofview.tactic list option) option ->
   (Id.t (* name of thm *) *
      (EConstr.types (* type of thm *) * (Name.t list (* names to pre-introduce *) * Impargs.manual_explicitation list))) list
-  -> int list option -> unit declaration_hook -> unit
+  -> int list option -> declaration_hook -> unit
 
 val universe_proof_terminator :
   Proof_global.lemma_possible_guards ->
-    (UState.t option -> unit declaration_hook) ->
+    (UState.t option -> declaration_hook) ->
     Proof_global.proof_terminator
 
 val standard_proof_terminator :
-  Proof_global.lemma_possible_guards -> unit declaration_hook ->
+  Proof_global.lemma_possible_guards -> declaration_hook ->
     Proof_global.proof_terminator
 
 val fresh_name_for_anonymous_theorem : unit -> Id.t
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index 757a56d436..bdf74bf63d 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -20,6 +20,14 @@ open Pp
 open CErrors
 open Util
 
+type univ_declaration_hook = UState.t -> Decl_kinds.locality -> GlobRef.t -> unit
+let mk_univ_hook f = f
+let call_univ_hook fix_exn hook uctx l c =
+  try hook uctx l c
+  with e when CErrors.noncritical e ->
+    let e = CErrors.push e in
+    iraise (fix_exn e)
+
 module NamedDecl = Context.Named.Declaration
 
 let get_fix_exn, stm_get_fix_exn = Hook.make ()
@@ -314,7 +322,7 @@ type program_info_aux = {
   prg_notations : notations ;
   prg_kind : definition_kind;
   prg_reduce : constr -> constr;
-  prg_hook : (UState.t -> unit) Lemmas.declaration_hook;
+  prg_hook : univ_declaration_hook;
   prg_opaque : bool;
   prg_sign: named_context_val;
 }
@@ -488,7 +496,7 @@ let declare_definition prg =
   let ubinders = UState.universe_binders uctx in
   DeclareDef.declare_definition prg.prg_name
     prg.prg_kind ce ubinders prg.prg_implicits
-    (Lemmas.mk_hook (fun l r -> Lemmas.call_hook fix_exn prg.prg_hook l r uctx; r))
+    (Lemmas.mk_hook (fun l r -> call_univ_hook fix_exn prg.prg_hook uctx l r ; ()))
 
 let rec lam_index n t acc =
   match Constr.kind t with
@@ -562,7 +570,7 @@ let declare_mutual_definition l =
     List.iter (Metasyntax.add_notation_interpretation (Global.env())) first.prg_notations;
     Declare.recursive_message (fixkind != IsCoFixpoint) indexes fixnames;
     let gr = List.hd kns in
-    Lemmas.call_hook fix_exn first.prg_hook local gr first.prg_ctx;
+    call_univ_hook fix_exn first.prg_hook first.prg_ctx local gr;
     List.iter progmap_remove l; gr
 
 let decompose_lam_prod c ty =
@@ -1099,7 +1107,7 @@ let show_term n =
 
 let add_definition n ?term t ctx ?(univdecl=UState.default_univ_decl)
                    ?(implicits=[]) ?(kind=Global,false,Definition) ?tactic
-    ?(reduce=reduce) ?(hook=Lemmas.mk_hook (fun _ _ _ -> ())) ?(opaque = false) obls =
+    ?(reduce=reduce) ?(hook=mk_univ_hook (fun _ _ _ -> ())) ?(opaque = false) obls =
   let sign = Lemmas.initialize_named_context_for_proof () in
   let info = Id.print n ++ str " has type-checked" in
   let prg = init_prog_info sign ~opaque n univdecl term t ctx [] None [] obls implicits kind reduce hook in
@@ -1119,7 +1127,7 @@ let add_definition n ?term t ctx ?(univdecl=UState.default_univ_decl)
 
 let add_mutual_definitions l ctx ?(univdecl=UState.default_univ_decl) ?tactic
                            ?(kind=Global,false,Definition) ?(reduce=reduce)
-    ?(hook=Lemmas.mk_hook (fun _ _ _ -> ())) ?(opaque = false) notations fixkind =
+    ?(hook=mk_univ_hook (fun _ _ _ -> ())) ?(opaque = false) notations fixkind =
   let sign = Lemmas.initialize_named_context_for_proof () in
   let deps = List.map (fun (n, b, t, imps, obls) -> n) l in
     List.iter
diff --git a/vernac/obligations.mli b/vernac/obligations.mli
index a37c30aafc..80294c7a76 100644
--- a/vernac/obligations.mli
+++ b/vernac/obligations.mli
@@ -13,6 +13,10 @@ open Constr
 open Evd
 open Names
 
+type univ_declaration_hook
+val mk_univ_hook : (UState.t -> Decl_kinds.locality -> GlobRef.t -> unit) -> univ_declaration_hook
+val call_univ_hook : Future.fix_exn -> univ_declaration_hook -> UState.t -> Decl_kinds.locality -> GlobRef.t -> unit
+
 (* This is a hack to make it possible for Obligations to craft a Qed
  * behind the scenes.  The fix_exn the Stm attaches to the Future proof
  * is not available here, so we provide a side channel to get it *)
@@ -59,7 +63,7 @@ val add_definition : Names.Id.t -> ?term:constr -> types ->
   ?kind:Decl_kinds.definition_kind ->
   ?tactic:unit Proofview.tactic ->
   ?reduce:(constr -> constr) ->
-  ?hook:(UState.t -> unit) Lemmas.declaration_hook -> ?opaque:bool -> obligation_info -> progress
+  ?hook:univ_declaration_hook -> ?opaque:bool -> obligation_info -> progress
 
 type notations =
     (lstring * Constrexpr.constr_expr * Notation_term.scope_name option) list
@@ -76,7 +80,7 @@ val add_mutual_definitions :
   ?tactic:unit Proofview.tactic ->
   ?kind:Decl_kinds.definition_kind ->
   ?reduce:(constr -> constr) ->
-  ?hook:(UState.t -> unit) Lemmas.declaration_hook -> ?opaque:bool ->
+  ?hook:univ_declaration_hook -> ?opaque:bool ->
   notations ->
   fixpoint_kind -> unit
 
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 24f6ba3049..32c61378db 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -479,10 +479,12 @@ let start_proof_and_print k l hook =
 let no_hook = Lemmas.mk_hook (fun _ _ -> ())
 
 let vernac_definition_hook p = function
-| Coercion -> Class.add_coercion_hook p
+| Coercion ->
+  Class.add_coercion_hook p
 | CanonicalStructure ->
-    Lemmas.mk_hook (fun _ -> Recordops.declare_canonical_structure)
-| SubClass -> Class.add_subclass_hook p
+  Lemmas.mk_hook (fun _ -> Recordops.declare_canonical_structure)
+| SubClass ->
+  Class.add_subclass_hook p
 | _ -> no_hook
 
 let vernac_definition ~atts discharge kind ({loc;v=id}, pl) def =