From 3429abee7c572676fa1155bf1620386bdf10d798 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 11 Oct 2018 00:20:24 +0200
Subject: [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.
---
 plugins/funind/functional_principles_proofs.ml | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'plugins/funind/functional_principles_proofs.ml')

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
-- 
cgit v1.2.3