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

(limited to 'vernac/declareDef.mli')

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