From d31056ec924ef6e09b28bc3822b427b67a8a300b Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Tue, 12 Feb 2019 22:37:33 +0100
Subject: [vernac] Unify declaration hooks.

Supersedes #8718.
---
 vernac/declareDef.ml | 14 ++++++++++----
 1 file changed, 10 insertions(+), 4 deletions(-)

(limited to 'vernac/declareDef.ml')

diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml
index 361ed1a737..7dcd098183 100644
--- a/vernac/declareDef.ml
+++ b/vernac/declareDef.ml
@@ -33,7 +33,7 @@ let get_locality id ~kind = function
 | Local -> true
 | Global -> false
 
-let declare_definition ident (local, p, k) ?hook ce pl imps =
+let declare_definition ident (local, p, k) ?hook_data ce pl imps =
   let fix_exn = Future.fix_exn_of ce.const_entry_body in
   let gr = match local with
   | Discharge when Lib.sections_are_opened () ->
@@ -49,11 +49,17 @@ let declare_definition ident (local, p, k) ?hook ce pl imps =
   in
   let () = maybe_declare_manual_implicits false gr imps in
   let () = definition_message ident in
-  Lemmas.call_hook ~fix_exn ?hook local gr; gr
+  begin
+    match hook_data with
+    | None -> ()
+    | Some (hook, uctx, extra_defs) ->
+      Lemmas.call_hook ~fix_exn ~hook uctx extra_defs local gr
+  end;
+  gr
 
-let declare_fix ?(opaque = false) (_,poly,_ as kind) pl univs f ((def,_),eff) t imps =
+let declare_fix ?(opaque = false) ?hook_data (_,poly,_ as kind) pl univs f ((def,_),eff) t imps =
   let ce = definition_entry ~opaque ~types:t ~univs ~eff def in
-  declare_definition f kind ce pl imps
+  declare_definition f kind ?hook_data ce pl imps
 
 let check_definition_evars ~allow_evars sigma =
   let env = Global.env () in
-- 
cgit v1.2.3