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.
---
 vernac/comFixpoint.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'vernac/comFixpoint.ml')

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