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/comDefinition.mli | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'vernac/comDefinition.mli')

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