[vernac] Remove unused abstraction from declaration_hook type.

"Declaration" hooks can be polymorphic on their return type, however
this facility doesn't seem used in the codebase.

We thus remove the polymorphism with the hope to be able to reify the
control later on.

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 =