Module Hook.S
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...
type t
=
{
uctx : UState.t;
ustate
: universe constraints obtained when the term was closedobls : (Names.Id.t * Constr.t) list;
(n1,t1),...(nm,tm)
: association list between obligation name and the corresponding defined term (might be a constant, but also an arbitrary term in the Expand case of obligations)scope : Locality.definition_scope;
scope
: Locality of the original declarationdref : Names.GlobRef.t;
dref
: identifier of the original declaration}