diff options
Diffstat (limited to 'plugins/funind/indfun_common.ml')
| -rw-r--r-- | plugins/funind/indfun_common.ml | 2 |
1 files changed, 1 insertions, 1 deletions
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 = |