[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.

8 files changed, 13 insertions, 19 deletions

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 =