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 closed

obls : (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.locality;

scope: Locality of the original declaration

dref : Names.GlobRef.t;

dref: identifier of the original declaration

}