Module Declare.Hook
Declaration hooks
module S : sig ... end
Hooks allow users of the API to perform arbitrary actions at proof/definition saving time. For example, to register a constant as a Coercion, perform some cleanup, update the search database, etc...