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.definition_scope;(*

scope: Locality of the original declaration

*)
dref : Names.GlobRef.t;(*

dref: identifier of the original declaration

*)
}