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

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

diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index f9938c0356..cba3cc3d42 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -129,7 +129,7 @@ let get_locality = function
 | Local -> true
 | Global -> false
 
-let save with_clean id const ?hook (locality,_,kind) =
+let save with_clean id const ?hook uctx (locality,_,kind) =
   let fix_exn = Future.fix_exn_of const.const_entry_body in
   let l,r = match locality with
     | Discharge when Lib.sections_are_opened () ->
@@ -144,7 +144,7 @@ let save with_clean id const ?hook (locality,_,kind) =
 	(locality, ConstRef kn)
   in
   if with_clean then Proof_global.discard_current ();
-  Lemmas.call_hook ?hook ~fix_exn l r;
+  Lemmas.call_hook ?hook ~fix_exn uctx [] l r;
   definition_message id
 
 let with_full_print f a =
-- 
cgit v1.2.3