[vernac] [hooks] Refactor towards optional hooks.

We make `declaration_hook`s optional arguments everywhere, and thus we
avoid some "fake" functions having to be passed.

This identifies positively the code really using hooks [funind,
rewrite, coercions, program, and canonicals] and helps moving toward
some hope of reification.

22 files changed, 137 insertions, 115 deletions

diff --git a/dev/ci/user-overlays/08705-ejgallego-vernac+remove_empty_hooks.sh b/dev/ci/user-overlays/08705-ejgallego-vernac+remove_empty_hooks.sh
new file mode 100644
index 0000000000..3600f1cd3e
--- /dev/null
+++ b/dev/ci/user-overlays/08705-ejgallego-vernac+remove_empty_hooks.sh
@@ -0,0 +1,18 @@
+if [ "$CI_PULL_REQUEST" = "8705" ] || [ "$CI_BRANCH" = "vernac+remove_empty_hooks" ]; then
+
+    elpi_CI_REF=vernac+remove_empty_hooks
+    elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi
+
+    equations_CI_REF=vernac+remove_empty_hooks
+    equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations
+
+    paramcoq_CI_REF=vernac+remove_empty_hooks
+    paramcoq_CI_GITURL=https://github.com/ejgallego/paramcoq
+
+    plugin_tutorial_CI_REF=vernac+remove_empty_hooks
+    plugin_tutorial_CI_GITURL=https://github.com/ejgallego/plugin_tutorials
+
+    mtac2_CI_REF=vernac+remove_empty_hooks
+    mtac2_CI_GITURL=https://github.com/ejgallego/mtac2
+
+fi
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index ef1d1af199..3b95423067 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -1005,8 +1005,7 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num
     (mk_equation_id f_id)
     (Decl_kinds.Global, false, (Decl_kinds.Proof Decl_kinds.Theorem))
     evd
-  lemma_type
-  (Lemmas.mk_hook (fun _ _ -> ()));
+  lemma_type;
   ignore (Pfedit.by (Proofview.V82.tactic prove_replacement));
   Lemmas.save_proof (Vernacexpr.(Proved(Proof_global.Transparent,None)));
   evd
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 5ba9735690..4cdfc6fac5 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -310,7 +310,6 @@ let build_functional_principle (evd:Evd.evar_map ref) interactive_proof old_prin
       (Decl_kinds.Global,false,(Decl_kinds.Proof Decl_kinds.Theorem))
       !evd
       (EConstr.of_constr new_principle_type)
-      hook
   ;
     (*       let _tim1 = System.get_time ()  in *)
       let map (c, u) = EConstr.mkConstU (c, EConstr.EInstance.make u) in
@@ -326,7 +325,7 @@ let build_functional_principle (evd:Evd.evar_map ref) interactive_proof old_prin
       match entries with
       | [entry] ->
         discard_current ();
-        (id,(entry,persistence)), CEphemeron.create hook
+        (id,(entry,persistence)), hook
       | _ ->
         CErrors.anomaly Pp.(str "[build_functional_principle] close_proof returned more than one proof term")
   end
@@ -386,7 +385,7 @@ let generate_functional_principle (evd: Evd.evar_map ref)
   (* Pr  1278 :
      Don't forget to close the goal if an error is raised !!!!
   *)
-  save false new_princ_name entry g_kind hook
+  save false new_princ_name entry g_kind ~hook
   with e when CErrors.noncritical e ->
     begin
       begin
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 35acbea488..3a04c753ea 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -415,7 +415,7 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp
         ~program_mode:false
 	fname
         (Decl_kinds.Global,false,Decl_kinds.Definition) pl
-	bl None body (Some ret_type) (Lemmas.mk_hook (fun _ _ -> ()));
+        bl None body (Some ret_type);
        let evd,rev_pconstants =
 	 List.fold_left
            (fun (evd,l) ((({CAst.v=fname},_),_,_,_,_),_) ->
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index c864bfe9f7..19f954c10d 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -129,7 +129,7 @@ let get_locality = function
 | Local -> true
 | Global -> false
 
-let save with_clean id const (locality,_,kind) hook =
+let save with_clean id const ?hook (locality,_,kind) =
   let fix_exn = Future.fix_exn_of const.const_entry_body in
   let l,r = match locality with
     | Discharge when Lib.sections_are_opened () ->
@@ -144,7 +144,7 @@ let save with_clean id const (locality,_,kind) hook =
 	(locality, ConstRef kn)
   in
   if with_clean then Proof_global.discard_current ();
-  CEphemeron.iter_opt hook (fun f -> Lemmas.call_hook fix_exn f l r);
+  Lemmas.call_hook ?hook ~fix_exn l r;
   definition_message id
 
 let with_full_print f a =
diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli
index c9d153d89f..9584649cff 100644
--- a/plugins/funind/indfun_common.mli
+++ b/plugins/funind/indfun_common.mli
@@ -42,8 +42,7 @@ val const_of_id: Id.t ->  GlobRef.t(* constantyes *)
 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 ->
-  Lemmas.declaration_hook CEphemeron.key -> unit
+val save : bool -> Id.t -> Safe_typing.private_constants Entries.definition_entry -> ?hook:Lemmas.declaration_hook -> Decl_kinds.goal_kind -> unit
 
 (* [with_full_print f a] applies [f] to [a] in full printing environment.
 
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index d1a227d517..95e2e9f6e5 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -806,8 +806,7 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list
 	   lem_id
            (Decl_kinds.Global,false,((Decl_kinds.Proof Decl_kinds.Theorem)))
            !evd
-	   typ
-           (Lemmas.mk_hook (fun _ _ -> ()));
+           typ;
 	 ignore (Pfedit.by
 		   (Proofview.V82.tactic (observe_tac ("prove correctness ("^(Id.to_string f_id)^")")
 						      (proving_tac i))));
@@ -867,8 +866,7 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list
 	 let lem_id = mk_complete_id f_id in
 	 Lemmas.start_proof lem_id
            (Decl_kinds.Global,false,(Decl_kinds.Proof Decl_kinds.Theorem)) sigma
-	 (fst lemmas_types_infos.(i))
-           (Lemmas.mk_hook (fun _ _ -> ()));
+         (fst lemmas_types_infos.(i));
 	 ignore (Pfedit.by
 	   (Proofview.V82.tactic (observe_tac ("prove completeness ("^(Id.to_string f_id)^")")
 	      (proving_tac i)))) ;
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 6e5e3f9353..38f27f760b 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -1372,7 +1372,7 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp
     na
     (Decl_kinds.Global, false (* FIXME *), Decl_kinds.Proof Decl_kinds.Lemma)
     sigma gls_type
-    (Lemmas.mk_hook hook);
+    ~hook:(Lemmas.mk_hook hook);
   if Indfun_common.is_strict_tcc  ()
   then
     ignore (by (Proofview.V82.tactic (tclIDTAC)))
@@ -1418,7 +1418,7 @@ let com_terminate
     let evd, env = Pfedit.get_current_context () in
     Lemmas.start_proof thm_name
       (Global, false (* FIXME *), Proof Lemma) ~sign:(Environ.named_context_val env)
-      ctx (EConstr.of_constr (compute_terminate_type nb_args fonctional_ref)) hook;
+      ctx (EConstr.of_constr (compute_terminate_type nb_args fonctional_ref)) ~hook;
 
     ignore (by (Proofview.V82.tactic (observe_tac (str "starting_tac") tac_start)));
     ignore (by (Proofview.V82.tactic (observe_tac (str "whole_start") (whole_start tac_end nb_args is_mes fonctional_ref
@@ -1474,8 +1474,7 @@ let (com_eqn : int -> Id.t ->
     (Lemmas.start_proof eq_name (Global, false, Proof Lemma)
        ~sign:(Environ.named_context_val env)
        evd
-       (EConstr.of_constr equation_lemma_type)
-       (Lemmas.mk_hook (fun _ _ -> ()));
+       (EConstr.of_constr equation_lemma_type);
      ignore (by
        (Proofview.V82.tactic (start_equation f_ref terminate_ref
 	  (fun  x ->
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index fee469032c..06783de614 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -1998,7 +1998,7 @@ let add_morphism_infer atts m n =
       let hook = Lemmas.mk_hook hook in
 	Flags.silently
 	  (fun () ->
-	    Lemmas.start_proof instance_id kind (Evd.from_ctx uctx) (EConstr.of_constr instance) hook;
+            Lemmas.start_proof ~hook instance_id kind (Evd.from_ctx uctx) (EConstr.of_constr instance);
 	    ignore (Pfedit.by (Tacinterp.interp tac))) ()
 
 let add_morphism atts binders m s n =
diff --git a/stm/stm.ml b/stm/stm.ml
index 94405924b7..3444229735 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1543,7 +1543,7 @@ end = struct (* {{{ *)
           let pobject, _ =
             Proof_global.close_future_proof ~opaque ~feedback_id:stop (Future.from_val ~fix_exn p) in
           let terminator = (* The one sent by master is an InvalidKey *)
-            Lemmas.(standard_proof_terminator [] (mk_hook (fun _ _ -> ()))) in
+            Lemmas.(standard_proof_terminator []) in
 
           let st = Vernacstate.freeze_interp_state `No in
           stm_vernac_interp stop
@@ -1682,9 +1682,8 @@ end = struct (* {{{ *)
         `OK_ADMITTED
       else begin
       (* The original terminator, a hook, has not been saved in the .vio*)
-      Proof_global.set_terminator
-        (Lemmas.standard_proof_terminator []
-           (Lemmas.mk_hook (fun _ _ -> ())));
+      Proof_global.set_terminator (Lemmas.standard_proof_terminator []);
+
       let opaque = Proof_global.Opaque in
       let proof =
         Proof_global.close_proof ~opaque ~keep_body_ucst_separate:true (fun x -> x) in
diff --git a/vernac/classes.ml b/vernac/classes.ml
index 7d6bd1ca64..d0cf1c6bee 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -163,10 +163,10 @@ 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 = Obligations.mk_univ_hook hook in
+    let univ_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)
+              ~univdecl:decl typ ctx ~kind:(Global,poly,Instance) ~univ_hook obls)
   else
     Flags.silently (fun () ->
         (* spiwack: it is hard to reorder the actions to do
@@ -176,7 +176,7 @@ let declare_instance_open env sigma ?hook ~tac ~program_mode ~global ~poly k id
         let gls = List.rev (Evd.future_goals sigma) in
         let sigma = Evd.reset_future_goals sigma in
         Lemmas.start_proof id ~pl:decl kind sigma (EConstr.of_constr termtype)
-          (Lemmas.mk_hook
+          ~hook:(Lemmas.mk_hook
              (fun _ -> instance_hook k pri global imps ?hook));
         (* spiwack: I don't know what to do with the status here. *)
         if not (Option.is_empty term) then
@@ -423,8 +423,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 _ _ -> ()) in
-        let _ = DeclareDef.declare_definition id decl entry UnivNames.empty_binders [] hook in
+        let _ = DeclareDef.declare_definition id decl entry UnivNames.empty_binders [] in
         Lib.sections_are_opened () || Lib.is_modtype_strict ()
       in
 	status && nstatus
diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml
index 9c80f1d2f5..79d45880fc 100644
--- a/vernac/comDefinition.ml
+++ b/vernac/comDefinition.ml
@@ -90,7 +90,7 @@ let check_definition (ce, evd, _, imps) =
   check_evars_are_solved env evd;
   ce
 
-let do_definition ~program_mode ident k univdecl bl red_option c ctypopt hook =
+let do_definition ~program_mode ?hook ident k univdecl bl red_option c ctypopt =
   let (ce, evd, univdecl, imps as def) =
     interp_definition univdecl bl (pi2 k) red_option c ctypopt
   in
@@ -108,8 +108,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 = Obligations.mk_univ_hook (fun _ _ l r -> Lemmas.call_hook (fun x -> x) hook l r) in
+      let univ_hook = Obligations.mk_univ_hook (fun _ _ l r -> Lemmas.call_hook ?hook l r) in
       ignore(Obligations.add_definition
-          ident ~term:c cty ctx ~univdecl ~implicits:imps ~kind:k ~hook obls)
+          ident ~term:c cty ctx ~univdecl ~implicits:imps ~kind:k ~univ_hook obls)
     else let ce = check_definition def in
-      ignore(DeclareDef.declare_definition ident k ce (Evd.universe_binders evd) imps hook)
+      ignore(DeclareDef.declare_definition ident k ce (Evd.universe_binders evd) imps ?hook)
diff --git a/vernac/comDefinition.mli b/vernac/comDefinition.mli
index 58007e6a88..0ac5762f71 100644
--- a/vernac/comDefinition.mli
+++ b/vernac/comDefinition.mli
@@ -17,9 +17,10 @@ open Constrexpr
 (** {6 Definitions/Let} *)
 
 val do_definition : program_mode:bool ->
+  ?hook:Lemmas.declaration_hook ->
   Id.t -> definition_kind -> universe_decl_expr option ->
   local_binder_expr list -> red_expr option -> constr_expr ->
-  constr_expr option -> Lemmas.declaration_hook -> unit
+  constr_expr option -> unit
 
 (************************************************************************)
 (** Internal API  *)
diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml
index 274c99107f..77227b64e6 100644
--- a/vernac/comFixpoint.ml
+++ b/vernac/comFixpoint.ml
@@ -261,7 +261,7 @@ let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) ind
         fixdefs) in
     let evd = Evd.from_ctx ctx in
     Lemmas.start_proof_with_initialization (local,poly,DefinitionBody Fixpoint)
-      evd pl (Some(false,indexes,init_tac)) thms None (Lemmas.mk_hook (fun _ _ -> ()))
+      evd pl (Some(false,indexes,init_tac)) thms None
   else begin
     (* We shortcut the proof process *)
     let fixdefs = List.map Option.get fixdefs in
@@ -296,7 +296,7 @@ let declare_cofixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) n
         fixdefs) in
     let evd = Evd.from_ctx ctx in
       Lemmas.start_proof_with_initialization (Global,poly, DefinitionBody CoFixpoint)
-      evd pl (Some(true,[],init_tac)) thms None (Lemmas.mk_hook (fun _ _ -> ()))
+      evd pl (Some(true,[],init_tac)) thms None
   else begin
     (* We shortcut the proof process *)
     let fixdefs = List.map Option.get fixdefs in
diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml
index ebedfb1e0d..e62ae99159 100644
--- a/vernac/comProgramFixpoint.ml
+++ b/vernac/comProgramFixpoint.ml
@@ -227,7 +227,7 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
       in hook, recname, typ
   in
   (* XXX: Capturing sigma here... bad bad *)
-  let hook = Obligations.mk_univ_hook (hook sigma) in
+  let univ_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
@@ -237,7 +237,7 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
   in
   let ctx = Evd.evar_universe_context sigma in
     ignore(Obligations.add_definition recname ~term:evars_def ~univdecl:decl
-             evars_typ ctx evars ~hook)
+             evars_typ ctx evars ~univ_hook)
 
 let out_def = function
   | Some def -> def
diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml
index 2fe03a8ec5..74b59735a9 100644
--- a/vernac/declareDef.ml
+++ b/vernac/declareDef.ml
@@ -33,7 +33,7 @@ let get_locality id ~kind = function
 | Local -> true
 | Global -> false
 
-let declare_definition ident (local, p, k) ce pl imps hook =
+let declare_definition ident (local, p, k) ?hook ce pl imps =
   let fix_exn = Future.fix_exn_of ce.const_entry_body in
   let gr = match local with
   | Discharge when Lib.sections_are_opened () ->
@@ -49,8 +49,8 @@ let declare_definition ident (local, p, k) ce pl imps hook =
   in
   let () = maybe_declare_manual_implicits false gr imps in
   let () = definition_message ident in
-  Lemmas.call_hook fix_exn hook local gr; gr
+  Lemmas.call_hook ~fix_exn ?hook local gr; gr
 
 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 _ _ -> ()))
+  declare_definition f kind ce pl imps
diff --git a/vernac/declareDef.mli b/vernac/declareDef.mli
index da11d4d9c0..b5dacf9ea0 100644
--- a/vernac/declareDef.mli
+++ b/vernac/declareDef.mli
@@ -14,8 +14,9 @@ open Decl_kinds
 val get_locality : Id.t -> kind:string -> Decl_kinds.locality -> bool
 
 val declare_definition : Id.t -> definition_kind ->
+  ?hook:Lemmas.declaration_hook ->
   Safe_typing.private_constants Entries.definition_entry -> UnivNames.universe_binders -> Impargs.manual_implicits ->
-  Lemmas.declaration_hook -> GlobRef.t
+  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 28e80a74aa..1a6eda446c 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -36,11 +36,12 @@ module NamedDecl = Context.Named.Declaration
 
 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
+let call_hook ?hook ?fix_exn l c =
+  try Option.iter (fun hook -> hook l c) hook
   with e when CErrors.noncritical e ->
     let e = CErrors.push e in
-    iraise (fix_exn e)
+    let e = Option.cata (fun fix -> fix e) e fix_exn in
+    iraise e
 
 (* Support for mutually proved theorems *)
 
@@ -202,7 +203,7 @@ let save ?export_seff id const uctx do_guard (locality,poly,kind) hook =
           gr
     in
     definition_message id;
-    call_hook (fun exn -> exn) hook locality r
+    call_hook ?hook locality r
   with e when CErrors.noncritical e ->
     let e = CErrors.push e in
     iraise (fix_exn e)
@@ -288,7 +289,7 @@ let warn_let_as_axiom =
                    (fun id -> strbrk "Let definition" ++ spc () ++ Id.print id ++
                                 spc () ++ strbrk "declared as an axiom.")
 
-let admit (id,k,e) pl hook () =
+let admit ?hook (id,k,e) pl () =
   let kn = declare_constant id (ParameterEntry e, IsAssumption Conjectural) in
   let () = match k with
   | Global, _, _ -> ()
@@ -296,16 +297,17 @@ let admit (id,k,e) pl hook () =
   in
   let () = assumption_message id in
   Declare.declare_univ_binders (ConstRef kn) pl;
-  call_hook (fun exn -> exn) hook Global (ConstRef kn)
+  call_hook ?hook Global (ConstRef kn)
 
 (* Starting a goal *)
 
-let universe_proof_terminator compute_guard hook =
+let universe_proof_terminator ?univ_hook compute_guard =
   let open Proof_global in
   make_terminator begin function
   | Admitted (id,k,pe,ctx) ->
-      admit (id,k,pe) (UState.universe_binders ctx) (hook (Some ctx)) ();
-      Feedback.feedback Feedback.AddedAxiom
+    let hook = Option.map (fun univ_hook -> univ_hook (Some ctx)) univ_hook in
+    admit ?hook (id,k,pe) (UState.universe_binders ctx) ();
+    Feedback.feedback Feedback.AddedAxiom
   | Proved (opaque,idopt, { id; entries=[const]; persistence; universes } ) ->
     let is_opaque, export_seff = match opaque with
       | Transparent -> false, true
@@ -315,13 +317,15 @@ let universe_proof_terminator compute_guard hook =
     let id = match idopt with
       | None -> id
       | Some { CAst.v = save_id } -> check_anonymity id save_id; save_id in
-    save ~export_seff id const universes compute_guard persistence (hook (Some universes))
+    let hook = Option.map (fun univ_hook -> univ_hook (Some universes)) univ_hook in
+    save ~export_seff id const universes compute_guard persistence hook
   | Proved (opaque,idopt, _ ) ->
     CErrors.anomaly Pp.(str "[universe_proof_terminator] close_proof returned more than one proof term")
   end
 
-let standard_proof_terminator compute_guard hook =
-  universe_proof_terminator compute_guard (fun _ -> hook)
+let standard_proof_terminator ?hook compute_guard =
+  let univ_hook = Option.map (fun hook _ -> hook) hook in
+  universe_proof_terminator ?univ_hook compute_guard
 
 let initialize_named_context_for_proof () =
   let sign = Global.named_context () in
@@ -331,10 +335,10 @@ let initialize_named_context_for_proof () =
       let d = if variable_opacity id then NamedDecl.LocalAssum (id, NamedDecl.get_type d) else d in
       Environ.push_named_context_val d signv) sign Environ.empty_named_context_val
 
-let start_proof id ?pl kind sigma ?terminator ?sign c ?(compute_guard=[]) hook =
+let start_proof id ?pl kind sigma ?terminator ?sign ?(compute_guard=[]) ?hook c =
   let terminator = match terminator with
-  | None -> standard_proof_terminator compute_guard hook
-  | Some terminator -> terminator compute_guard hook
+  | None -> standard_proof_terminator ?hook compute_guard
+  | Some terminator -> terminator ?hook compute_guard
   in
   let sign = 
     match sign with
@@ -344,10 +348,11 @@ let start_proof id ?pl kind sigma ?terminator ?sign c ?(compute_guard=[]) hook =
   let goals = [ Global.env_of_context sign , c ] in
   Proof_global.start_proof sigma id ?pl kind goals terminator
 
-let start_proof_univs id ?pl kind sigma ?terminator ?sign c ?(compute_guard=[]) hook =
+let start_proof_univs id ?pl kind sigma ?terminator ?sign ?(compute_guard=[]) ?univ_hook c =
   let terminator = match terminator with
-  | None -> universe_proof_terminator compute_guard hook
-  | Some terminator -> terminator compute_guard hook
+  | None ->
+    universe_proof_terminator ?univ_hook compute_guard
+  | Some terminator -> terminator ?univ_hook compute_guard
   in
   let sign =
     match sign with
@@ -371,7 +376,7 @@ let rec_tac_initializer finite guard thms snl =
        | (id,n,_)::l -> Tactics.mutual_fix id n l 0
        | _ -> assert false
 
-let start_proof_with_initialization kind sigma decl recguard thms snl hook =
+let start_proof_with_initialization ?hook kind sigma decl recguard thms snl =
   let intro_tac (_, (_, (ids, _))) = Tactics.auto_intros_tac ids in
   let init_tac,guard = match recguard with
   | Some (finite,guard,init_tac) ->
@@ -405,14 +410,14 @@ let start_proof_with_initialization kind sigma decl recguard thms snl hook =
         let thms_data = (strength,ref,imps)::other_thms_data in
         List.iter (fun (strength,ref,imps) ->
 	  maybe_declare_manual_implicits false ref imps;
-	  call_hook (fun exn -> exn) hook strength ref) thms_data in
-      start_proof_univs id ~pl:decl kind sigma t (fun ctx -> mk_hook (hook ctx)) ~compute_guard:guard;
+          call_hook ?hook strength ref) thms_data in
+      start_proof_univs id ~pl:decl kind sigma t ~univ_hook:(fun ctx -> mk_hook (hook ctx)) ~compute_guard:guard;
       ignore (Proof_global.with_current_proof (fun _ p ->
           match init_tac with
           | None -> p,(true,[])
           | Some tac -> Proof.run_tactic Global.(env ()) tac p))
 
-let start_proof_com ?inference_hook kind thms hook =
+let start_proof_com ?inference_hook ?hook kind thms =
   let env0 = Global.env () in
   let decl = fst (List.hd thms) in
   let evd, decl = Constrexpr_ops.interp_univ_decl_opt env0 (snd decl) in
@@ -444,7 +449,7 @@ let start_proof_com ?inference_hook kind thms hook =
     else (* We fix the variables to ensure they won't be lowered to Set *)
       Evd.fix_undefined_variables evd
   in
-    start_proof_with_initialization kind evd decl recguard thms snl hook
+    start_proof_with_initialization ?hook kind evd decl recguard thms snl
 
 (* Saving a proof *)
 
diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli
index 246d8cbe6d..3ac12d3b0b 100644
--- a/vernac/lemmas.mli
+++ b/vernac/lemmas.mli
@@ -12,41 +12,45 @@ open Names
 open Decl_kinds
 
 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 call_hook :
+  ?hook:declaration_hook -> ?fix_exn:Future.fix_exn ->
+  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 -> declaration_hook -> Proof_global.proof_terminator) ->
-  ?sign:Environ.named_context_val -> EConstr.types ->
+  ?terminator:(?hook:declaration_hook -> Proof_global.lemma_possible_guards -> Proof_global.proof_terminator) ->
+  ?sign:Environ.named_context_val ->
   ?compute_guard:Proof_global.lemma_possible_guards ->
-  declaration_hook -> unit
+  ?hook:declaration_hook ->  EConstr.types -> 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 -> declaration_hook) -> Proof_global.proof_terminator) ->
-  ?sign:Environ.named_context_val -> EConstr.types ->
+  ?terminator:(?univ_hook:(UState.t option -> declaration_hook) -> Proof_global.lemma_possible_guards -> Proof_global.proof_terminator) ->
+  ?sign:Environ.named_context_val ->
   ?compute_guard:Proof_global.lemma_possible_guards ->
-  (UState.t option -> declaration_hook) -> unit
+  ?univ_hook:(UState.t option -> declaration_hook) -> EConstr.types -> unit
 
 val start_proof_com :
   ?inference_hook:Pretyping.inference_hook ->
-  goal_kind -> Vernacexpr.proof_expr list ->
-  declaration_hook -> unit
+  ?hook:declaration_hook -> goal_kind -> Vernacexpr.proof_expr list ->
+  unit
 
 val start_proof_with_initialization :
+  ?hook:declaration_hook ->
   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 -> declaration_hook -> unit
+     (EConstr.types (* type of thm *) * (Name.t list (* names to pre-introduce *) * Impargs.manual_explicitation list))) list ->
+  int list option -> unit
 
 val universe_proof_terminator :
+  ?univ_hook:(UState.t option -> declaration_hook) ->
   Proof_global.lemma_possible_guards ->
-    (UState.t option -> declaration_hook) ->
-    Proof_global.proof_terminator
+  Proof_global.proof_terminator
 
 val standard_proof_terminator :
-  Proof_global.lemma_possible_guards -> declaration_hook ->
-    Proof_global.proof_terminator
+  ?hook:declaration_hook -> Proof_global.lemma_possible_guards ->
+  Proof_global.proof_terminator
 
 val fresh_name_for_anonymous_theorem : unit -> Id.t
 
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index 4926b8c3e1..f18227039f 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -22,11 +22,12 @@ open Util
 
 type univ_declaration_hook = UState.t -> (Id.t * constr) list -> Decl_kinds.locality -> GlobRef.t -> unit
 let mk_univ_hook f = f
-let call_univ_hook fix_exn hook uctx trans l c =
-  try hook uctx trans l c
+let call_univ_hook ?univ_hook ?fix_exn uctx trans l c =
+  try Option.iter (fun hook -> hook uctx trans l c) univ_hook
   with e when CErrors.noncritical e ->
     let e = CErrors.push e in
-    iraise (fix_exn e)
+    let e = Option.cata (fun fix -> fix e) e fix_exn in
+    iraise e
 
 module NamedDecl = Context.Named.Declaration
 
@@ -320,7 +321,7 @@ type program_info_aux = {
   prg_notations : notations ;
   prg_kind : definition_kind;
   prg_reduce : constr -> constr;
-  prg_hook : univ_declaration_hook;
+  prg_hook : univ_declaration_hook option;
   prg_opaque : bool;
   prg_sign: named_context_val;
 }
@@ -481,9 +482,9 @@ let declare_definition prg =
   let ce = definition_entry ~fix_exn ~opaque ~types:typ ~univs body in
   let () = progmap_remove prg in
   let ubinders = UState.universe_binders uctx in
+  let hook = Lemmas.mk_hook (fun l r -> call_univ_hook ?univ_hook:prg.prg_hook ~fix_exn uctx obls l r; ()) in
   DeclareDef.declare_definition prg.prg_name
-    prg.prg_kind ce ubinders prg.prg_implicits
-    (Lemmas.mk_hook (fun l r -> call_univ_hook fix_exn prg.prg_hook uctx obls l r ; ()))
+    prg.prg_kind ce ubinders prg.prg_implicits ~hook
 
 let rec lam_index n t acc =
   match Constr.kind t with
@@ -564,7 +565,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
-    call_univ_hook fix_exn first.prg_hook first.prg_ctx obls local gr;
+    call_univ_hook ?univ_hook:first.prg_hook ~fix_exn first.prg_ctx obls local gr;
     List.iter progmap_remove l; gr
 
 let decompose_lam_prod c ty =
@@ -662,8 +663,8 @@ let declare_obligation prg obl body ty uctx =
       in
       true, { obl with obl_body = body }
 
-let init_prog_info ?(opaque = false) sign n udecl b t ctx deps fixkind
-		   notations obls impls kind reduce hook =
+let init_prog_info ?(opaque = false) ?univ_hook sign n udecl b t ctx deps fixkind
+                   notations obls impls kind reduce =
   let obls', b =
     match b with
     | None ->
@@ -688,7 +689,7 @@ let init_prog_info ?(opaque = false) sign n udecl b t ctx deps fixkind
       prg_obligations = (obls', Array.length obls');
       prg_deps = deps; prg_fixkind = fixkind ; prg_notations = notations ;
       prg_implicits = impls; prg_kind = kind; prg_reduce = reduce; 
-      prg_hook = hook; prg_opaque = opaque;
+      prg_hook = univ_hook; prg_opaque = opaque;
       prg_sign = sign }
 
 let map_cardinal m =
@@ -843,9 +844,9 @@ let solve_by_tac ?loc name evi t poly ctx =
     warn_solve_errored ?loc err;
     None
 
-let obligation_terminator name num guard hook auto pf =
+let obligation_terminator ?univ_hook name num guard auto pf =
   let open Proof_global in
-  let term = Lemmas.universe_proof_terminator guard hook in
+  let term = Lemmas.universe_proof_terminator ?univ_hook guard in
   match pf with
   | Admitted _ -> apply_terminator term pf
   | Proved (opq, id, { entries=[entry]; universes=uctx } ) -> begin
@@ -968,11 +969,11 @@ let rec solve_obligation prg num tac =
   let evd = Evd.from_ctx prg.prg_ctx in
   let evd = Evd.update_sigma_env evd (Global.env ()) in
   let auto n tac oblset = auto_solve_obligations n ~oblset tac in
-  let terminator guard hook =
+  let terminator ?univ_hook guard =
     Proof_global.make_terminator
-      (obligation_terminator prg.prg_name num guard hook auto) in
-  let hook ctx = Lemmas.mk_hook (obligation_hook prg obl num auto ctx) in
-  let () = Lemmas.start_proof_univs ~sign:prg.prg_sign obl.obl_name kind evd (EConstr.of_constr obl.obl_type) ~terminator hook in
+      (obligation_terminator ?univ_hook prg.prg_name num guard auto) in
+  let univ_hook ctx = Lemmas.mk_hook (obligation_hook prg obl num auto ctx) in
+  let () = Lemmas.start_proof_univs ~sign:prg.prg_sign obl.obl_name kind evd (EConstr.of_constr obl.obl_type) ~terminator ~univ_hook in
   let _ = Pfedit.by !default_tactic in
   Option.iter (fun tac -> Proof_global.set_endline_tactic tac) tac
 
@@ -1109,10 +1110,10 @@ 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=mk_univ_hook (fun _ _ _ _ -> ())) ?(opaque = false) obls =
+    ?(reduce=reduce) ?univ_hook ?(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
+  let prg = init_prog_info sign ~opaque n univdecl term t ctx [] None [] obls implicits kind reduce ?univ_hook in
   let obls,_ = prg.prg_obligations in
   if Int.equal (Array.length obls) 0 then (
     Flags.if_verbose Feedback.msg_info (info ++ str ".");
@@ -1129,13 +1130,13 @@ 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=mk_univ_hook (fun _ _ _ _ -> ())) ?(opaque = false) notations fixkind =
+    ?univ_hook ?(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
     (fun  (n, b, t, imps, obls) ->
      let prg = init_prog_info sign ~opaque n univdecl (Some b) t ctx deps (Some fixkind)
-       notations obls imps kind reduce hook 
+       notations obls imps kind reduce ?univ_hook
      in progmap_add n (CEphemeron.create prg)) l;
     let _defined =
       List.fold_left (fun finished x ->
diff --git a/vernac/obligations.mli b/vernac/obligations.mli
index 57040b3f7c..c670e3a3b5 100644
--- a/vernac/obligations.mli
+++ b/vernac/obligations.mli
@@ -14,8 +14,10 @@ open Evd
 open Names
 
 type univ_declaration_hook
-val mk_univ_hook : (UState.t -> (Id.t * constr) list -> Decl_kinds.locality -> GlobRef.t -> unit) -> univ_declaration_hook
-val call_univ_hook : Future.fix_exn -> univ_declaration_hook -> UState.t -> (Id.t * constr) list -> Decl_kinds.locality -> GlobRef.t -> unit
+val mk_univ_hook : (UState.t -> (Id.t * constr) list -> Decl_kinds.locality -> GlobRef.t -> unit) ->
+  univ_declaration_hook
+val call_univ_hook : ?univ_hook:univ_declaration_hook -> ?fix_exn:Future.fix_exn ->
+  UState.t -> (Id.t * constr) list -> 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
@@ -56,14 +58,14 @@ type progress = (* Resolution status of a program *)
 
 val default_tactic : unit Proofview.tactic ref
 
-val add_definition : Names.Id.t -> ?term:constr -> types -> 
+val add_definition : Names.Id.t -> ?term:constr -> types ->
   UState.t ->
   ?univdecl:UState.universe_decl -> (* Universe binders and constraints *)
   ?implicits:(Constrexpr.explicitation * (bool * bool * bool)) list ->
   ?kind:Decl_kinds.definition_kind ->
   ?tactic:unit Proofview.tactic ->
   ?reduce:(constr -> constr) ->
-  ?hook:univ_declaration_hook -> ?opaque:bool -> obligation_info -> progress
+  ?univ_hook:univ_declaration_hook -> ?opaque:bool -> obligation_info -> progress
 
 type notations =
     (lstring * Constrexpr.constr_expr * Notation_term.scope_name option) list
@@ -80,7 +82,7 @@ val add_mutual_definitions :
   ?tactic:unit Proofview.tactic ->
   ?kind:Decl_kinds.definition_kind ->
   ?reduce:(constr -> constr) ->
-  ?hook:univ_declaration_hook -> ?opaque:bool ->
+  ?univ_hook:univ_declaration_hook -> ?opaque:bool ->
   notations ->
   fixpoint_kind -> unit
 
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index a157e01fc1..991111ddde 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -475,7 +475,7 @@ let vernac_custom_entry ~module_local s =
 (***********)
 (* Gallina *)
 
-let start_proof_and_print k l hook =
+let start_proof_and_print ?hook k l =
   let inference_hook =
     if Flags.is_program_mode () then
       let hook env sigma ev =
@@ -497,18 +497,16 @@ let start_proof_and_print k l hook =
       in Some hook
     else None
   in
-  start_proof_com ?inference_hook k l hook
-
-let no_hook = Lemmas.mk_hook (fun _ _ -> ())
+  start_proof_com ?inference_hook ?hook k l
 
 let vernac_definition_hook p = function
 | Coercion ->
-  Class.add_coercion_hook p
+  Some (Class.add_coercion_hook p)
 | CanonicalStructure ->
-  Lemmas.mk_hook (fun _ -> Recordops.declare_canonical_structure)
+  Some (Lemmas.mk_hook (fun _ -> Recordops.declare_canonical_structure))
 | SubClass ->
-  Class.add_subclass_hook p
-| _ -> no_hook
+  Some (Class.add_subclass_hook p)
+| _ -> None
 
 let vernac_definition ~atts discharge kind ({loc;v=id}, pl) def =
   let atts = attributes_of_flags atts in
@@ -531,7 +529,7 @@ let vernac_definition ~atts discharge kind ({loc;v=id}, pl) def =
   (match def with
     | ProveBody (bl,t) ->   (* local binders, typ *)
       start_proof_and_print (local, atts.polymorphic, DefinitionBody kind)
-        [(CAst.make ?loc name, pl), (bl, t)] hook
+        ?hook [(CAst.make ?loc name, pl), (bl, t)]
     | DefineBody (bl,red_option,c,typ_opt) ->
       let red_option = match red_option with
           | None -> None
@@ -539,14 +537,14 @@ let vernac_definition ~atts discharge kind ({loc;v=id}, pl) def =
             let sigma, env = Pfedit.get_current_context () in
             Some (snd (Hook.get f_interp_redexp env sigma r)) in
       ComDefinition.do_definition ~program_mode name
-        (local, atts.polymorphic, kind) pl bl red_option c typ_opt hook)
+        (local, atts.polymorphic, kind) pl bl red_option c typ_opt ?hook)
 
 let vernac_start_proof ~atts kind l =
   let atts = attributes_of_flags atts in
   let local = enforce_locality_exp atts.locality NoDischarge in
   if Dumpglob.dump () then
     List.iter (fun ((id, _), _) -> Dumpglob.dump_definition id false "prf") l;
-  start_proof_and_print (local, atts.polymorphic, Proof kind) l no_hook
+  start_proof_and_print (local, atts.polymorphic, Proof kind) l
 
 let vernac_end_proof ?proof = function
   | Admitted          -> save_proof ?proof Admitted