From 873281c256fc33941d93044acc3db8eda0a148ee Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sun, 24 Feb 2019 20:38:21 +0100
Subject: [proof] Move declaration hooks to DeclareDef.

This way both `Lemmas` and `DeclareObl` can depend on it, removing one
more difficulty on the unification of terminators.
---
 plugins/funind/indfun_common.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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

diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 7683ce1757..732a0d818f 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -137,7 +137,7 @@ let save id const ?hook uctx (locality,_,kind) =
         let kn = declare_constant id ~local (DefinitionEntry const, k) in
         ConstRef kn
   in
-  Lemmas.call_hook ?hook ~fix_exn uctx [] locality r;
+  DeclareDef.Hook.call ?hook ~fix_exn uctx [] locality r;
   definition_message id
 
 let with_full_print f a =
-- 
cgit v1.2.3